Theory GenCF_No_Comp

section ‹Generic Collection Framework (Internal)›
theory GenCF_No_Comp
imports
  Collections.Impl_List_Set
  Collections.Impl_List_Map
  Collections.Impl_RBT_Map
  Collections.Impl_Array_Map
  Collections.Impl_Array_Hash_Map
  Collections.Impl_Array_Stack
  Collections.Impl_Cfun_Set
  Collections.Impl_Bit_Set
  Collections.Impl_Uv_Set
  Collections.Gen_Set
  Collections.Gen_Map
  Collections.Gen_Map2Set
  Collections.Gen_Hash
  Collections.Code_Target_ICF
  Automatic_Refinement.Refine_Lib
  "HOL-Analysis.Analysis"
begin

  text ‹TODO: need to keep in sync with ‹../../Collections/GenCF/CenCF› ...›

  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