section ‹\isaheader{Generic Collection Framework (Internal)}› theory GenCF imports "Impl/Impl_List_Set" "Impl/Impl_List_Map" "Impl/Impl_RBT_Map" "Impl/Impl_Array_Map" "Impl/Impl_Array_Hash_Map" "Impl/Impl_Array_Stack" "Impl/Impl_Cfun_Set" "Impl/Impl_Bit_Set" "Impl/Impl_Uv_Set" "Gen/Gen_Set" "Gen/Gen_Map" "Gen/Gen_Map2Set" "Gen/Gen_Comp" "Gen/Gen_Hash" "../Lib/Code_Target_ICF" begin text ‹Use one of the ‹Refine_Dflt›-theories as entry-point!› text ‹Useful Abbreviations› abbreviation "dflt_rs_rel ≡ map2set_rel dflt_rm_rel" abbreviation "iam_set_rel ≡ map2set_rel iam_map_rel" abbreviation "dflt_ahs_rel ≡ map2set_rel dflt_ahm_rel" abbreviation ahs_rel where "ahs_rel bhc ≡ (map2set_rel (ahm_rel bhc))" end