Session Nested_Multisets_Ordinals

Theories

• 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
• HOL-Library.Sublist
• Multiset_More
• Signed_Multiset
  • File ‹zmultiset_simprocs.ML›
• Nested_Multiset
• Hereditary_Multiset
• Signed_Hereditary_Multiset
• HOL-Library.Product_Plus
• HOL-Library.Product_Order
• 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.Infinite_Set
• HOL-Library.Countable_Set
• HOL-Library.Countable_Complete_Lattices
• HOL-Library.Order_Continuity
• HOL-Library.Extended_Nat
• Syntactic_Ordinal
• Signed_Syntactic_Ordinal
• Syntactic_Ordinal_Bridge
• McCarthy_91
• Hydra_Battle
• Goodstein_Sequence
• HOL-Library.FSet
• HOL-Library.Countable_Set_Type
• List-Index.List_Index
• Unary_PCF