Session Virtual_Substitution
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Groups_Big_Fun
HOL-Library.Fun_Lexorder
HOL-Library.More_List
HOL-Library.Poly_Mapping
Polynomials.MPoly_Type
Polynomials.More_MPoly_Type
HOL-Computational_Algebra.Polynomial
Polynomials.MPoly_Type_Univariate
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
Abstract-Rewriting.Abstract_Rewriting
Abstract-Rewriting.SN_Orders
Matrix.Utility
Polynomials.Polynomials
HOL-Library.Sublist
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
Polynomials.Utils
HOL-Library.Function_Algebras
Well_Quasi_Orders.Well_Quasi_Orders
Polynomials.Power_Products
Polynomials.More_Modules
Polynomials.MPoly_Type_Class
Polynomials.MPoly_Type_Class_Ordered
HOL-Library.FSet
HOL-Library.AList
HOL-Library.Conditional_Parametricity
File ‹conditional_parametricity.ML›
HOL-Library.Finite_Map
Polynomials.Poly_Mapping_Finite_Map
Polynomials.MPoly_Type_Class_FMap
HOL-Library.Quadratic_Discriminant
QE
MPolyExtension
ExecutiblePolyProps
PolyAtoms
Debruijn
Reindex
Optimizations
OptimizationProofs
VSAlgos
Heuristic
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
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
Polynomials.Show_Polynomials
PrettyPrinting
Show.Show_Real
Exports
LinearCase
QuadraticCase
EliminateVariable
LuckyFind
EqualityVS
UniAtoms
NegInfinity
NegInfinityUni
Infinitesimals
InfinitesimalsUni
DNFUni
GeneralVSProofs
DNF
VSQuad
HeuristicProofs
ExportProofs