Theory Refine_Dflt_Only_ICF

section ‹\isaheader{Entry Point with only the ICF}›
theory Refine_Dflt_Only_ICF
imports
  Refine_Monadic.Refine_Monadic
  "ICF/Collections"
  "Lib/Code_Target_ICF"
begin

text ‹Contains the Monadic Refinement Framework and the original
  Isabelle Collection Framework. The generic collection framework is
  not included›

local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "RBT-set" @{term "⟨R⟩rs.rel"} PR_LAST #>
    declare_prio "Hash-set" @{term "⟨R⟩hs.rel"} PR_LAST #>
    declare_prio "List-set" @{term "⟨R⟩lsi.rel"} PR_LAST
  end
›

local_setup ‹
  let open Autoref_Fix_Rel in
    declare_prio "RBT-map" @{term "⟨Rk,Rv⟩rm.rel"} PR_LAST #>
    declare_prio "Hash-map" @{term "⟨Rk,Rv⟩hm.rel"} PR_LAST #>
    declare_prio "List-map" @{term "⟨Rk,Rv⟩lmi.rel"} PR_LAST
  end
›

end