Session PAC_Checker
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
HOL-Library.FuncSet
HOL-Algebra.Congruence
HOL-Algebra.Order
HOL-Algebra.Lattice
HOL-Algebra.Complete_Lattice
HOL-Algebra.Group
HOL-Algebra.FiniteProduct
HOL-Algebra.Ring
File ‹ringsimp.ML›
HOL-Algebra.Coset
HOL-Algebra.AbelCoset
HOL-Algebra.Ideal
HOL-Library.Disjoint_Sets
HOL-Combinatorics.Transposition
HOL-Combinatorics.Permutations
HOL-Combinatorics.List_Permutation
HOL-Algebra.Divisibility
HOL-Algebra.RingHom
HOL-Algebra.QuotRing
HOL-Algebra.Module
HOL-Algebra.UnivPoly
HOL-Algebra.Generated_Groups
HOL-Algebra.Elementary_Groups
HOL-Algebra.Multiplicative_Group
HOL-Algebra.Ring_Divisibility
HOL-Algebra.Subrings
HOL-Algebra.Polynomials
HOL-Library.Sublist
HOL-Library.Ramsey
Regular-Sets.Regular_Set
Regular-Sets.Regular_Exp
Regular-Sets.NDerivative
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
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
HOL-Library.Countable_Set
PAC_More_Poly
HOL-Library.FSet
HOL-Library.Conditional_Parametricity
File ‹conditional_parametricity.ML›
HOL-Library.Finite_Map
HOL-Library.Multiset_Order
Nested_Multisets_Ordinals.Multiset_More
Nested_Multisets_Ordinals.Duplicate_Free_Multiset
Finite_Map_Multiset
WB_Sort
More_Loops
PAC_Specification
PAC_Map_Rel
PAC_Checker_Specification
PAC_Polynomials
PAC_Polynomials_Term
PAC_Polynomials_Operations
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
PAC_Misc
PAC_Checker
Native_Word.Uint64
PAC_Checker_Relation
PAC_Assoc_Map_Rel
PAC_Checker_Init
PAC_Version
PAC_Checker_Synthesis
PAC_Checker_MLton