Session Polynomials

Theories

• HOL-Library.AList
• 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
• Open_Induction.Restricted_Predicates
• Well_Quasi_Orders.Almost_Full
• Well_Quasi_Orders.Minimal_Elements
• Well_Quasi_Orders.Minimal_Bad_Sequences
• Well_Quasi_Orders.Almost_Full_Relations
• Utils
• HOL-Library.Function_Algebras
• HOL-Library.Groups_Big_Fun
• HOL-Library.Fun_Lexorder
• HOL-Library.More_List
• HOL-Library.Poly_Mapping
• MPoly_Type
• More_MPoly_Type
• Well_Quasi_Orders.Well_Quasi_Orders
• Power_Products
• More_Modules
• MPoly_Type_Class
• MPoly_Type_Class_Ordered
• HOL-Library.FSet
• HOL-Library.Conditional_Parametricity
  • File ‹conditional_parametricity.ML›
• HOL-Library.Finite_Map
• Poly_Mapping_Finite_Map
• MPoly_Type_Class_FMap
• PP_Type
• Deriving.Comparator
• OAlist
• OAlist_Poly_Mapping
• HOL-Library.Product_Lexorder
• Term_Order
• MPoly_Type_Class_OAlist
• Quasi_PM_Power_Products
• MPoly_PM
• 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-Computational_Algebra.Factorial_Ring
• HOL-Computational_Algebra.Euclidean_Algorithm
• HOL-Computational_Algebra.Primes
• HOL-Computational_Algebra.Polynomial
• MPoly_Type_Univariate
• Matrix.Utility
• Polynomials
• Deriving.Generator_Aux
  • File ‹bnf_access.ML›
  • File ‹generator_aux.ML›
• Deriving.Derive_Manager
  • File ‹derive_manager.ML›
• Show.Show
  • File ‹show_generator.ML›
• Show.Show_Instances
• Show_Polynomials
• NZM