Session More_Refinement_Libs

Theories

• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.FSet
• HOL-Library.AList
• HOL-Library.Conditional_Parametricity
  • File ‹conditional_parametricity.ML›
• HOL-Library.Finite_Map
• HOL-Library.Multiset_Order
• HOL-Library.Sublist
• Nested_Multisets_Ordinals.Multiset_More
• Nested_Multisets_Ordinals.Duplicate_Free_Multiset
• HOL-Eisbach.Eisbach_Tools
• HOL-Library.FuncSet
• Weidenbach_Book_Base.WB_List_More
• HOL-Library.Rewrite
  • File ‹cconv.ML›
  • File ‹rewrite.ML›
• WB_More_Refinement_Loops