Session Groebner_Bases

Theories

• HOL-Library.Sublist
• HOL-Library.Ramsey
• Regular-Sets.Regular_Set
• Regular-Sets.Regular_Exp
• Regular-Sets.NDerivative
• HOL-Library.While_Combinator
• Regular-Sets.Equivalence_Checking
• Regular-Sets.Relation_Interpretation
• Regular-Sets.Regexp_Method
• Abstract-Rewriting.Seq
• 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
• Polynomials.Utils
• General
• HOL-Library.Function_Algebras
• Polynomials.MPoly_Type
• Polynomials.More_MPoly_Type
• Well_Quasi_Orders.Well_Quasi_Orders
• Polynomials.Power_Products
• Polynomials.More_Modules
• Polynomials.MPoly_Type_Class
• Polynomials.MPoly_Type_Class_Ordered
• Abstract-Rewriting.Abstract_Rewriting
• Confluence
• Reduction
• Groebner_Bases
• Algorithm_Schema
• Buchberger
• Polynomials.PP_Type
• Deriving.Comparator
• Polynomials.OAlist
• Polynomials.OAlist_Poly_Mapping
• HOL-Library.Product_Lexorder
• Polynomials.Term_Order
• Polynomials.MPoly_Type_Class_OAlist
• Benchmarks
• Algorithm_Schema_Impl
• Code_Target_Rat
• Buchberger_Examples
• More_MPoly_Type_Class
• Auto_Reduction
• Reduced_GB
• Reduced_GB_Examples
• Polynomial_Interpolation.Ring_Hom
• Jordan_Normal_Form.Missing_Misc
• Jordan_Normal_Form.Missing_Ring
• HOL-Library.Complex_Order
• Jordan_Normal_Form.Conjugate
• Jordan_Normal_Form.Matrix
• Jordan_Normal_Form.Gauss_Jordan_Elimination
• Macaulay_Matrix
• F4
• Polynomial_Interpolation.Missing_Unsorted
• HOL-Library.IArray
• Jordan_Normal_Form.Matrix_IArray_Impl
• Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
• F4_Examples
• Syzygy
• Syzygy_Examples
• Polynomials.Quasi_PM_Power_Products
• Polynomials.MPoly_PM
• Groebner_PM