Session Decreasing-Diagrams-II

Theories

• Open_Induction.Restricted_Predicates
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• Well_Quasi_Orders.Multiset_Extension
• HOL-Library.FuncSet
• 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.Countable_Set
• HOL-Library.Equipollence
• HOL-Library.Ramsey
• Well_Quasi_Orders.Least_Enum
• Well_Quasi_Orders.Infinite_Sequences
• Well_Quasi_Orders.Almost_Full
• Well_Quasi_Orders.Minimal_Elements
• Well_Quasi_Orders.Minimal_Bad_Sequences
• Well_Quasi_Orders.Almost_Full_Relations
• Well_Quasi_Orders.Well_Quasi_Orders
• Decreasing_Diagrams_II_Aux
• HOL-Cardinals.Order_Union
• HOL-Cardinals.Wellorder_Extension
• Decreasing_Diagrams_II