Session Higher_Order_Terms

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.Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• HOL-Library.Monad_Syntax
• HOL-Library.State_Monad
• Term_Utils
• List-Index.List_Index
• Find_First
• Name
• Fresh_Monad
• Fresh_Class
• Deriving.Derive_Manager
  • File ‹derive_manager.ML›
• Datatype_Order_Generator.Derive_Aux
  • File ‹derive_aux.ML›
• Datatype_Order_Generator.Order_Generator
  • File ‹order_generator.ML›
• HOL-Library.FuncSet
• HOL-Library.Disjoint_Sets
• HOL-Library.Disjoint_FSets
• Term_Class
• Term
• Pats
• Nterm
• Term_to_Nterm
• HOL-ex.Unification
• Unification_Compat
• HOL-Library.Infinite_Set
• HOL-Library.Countable_Set
• HOL-Library.Countable_Complete_Lattices
• HOL-Library.Order_Continuity
• HOL-Library.Extended_Nat
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• HOL-Library.Multiset_Order
• Lambda_Free_RPOs.Lambda_Free_Util
• Lambda_Free_RPOs.Lambda_Free_Term
• Lambda_Free_Compat