Session FO_Theory_Rewriting
View
theory dependencies
View
document
View
outline
Theories
First_Order_Terms.Term
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
Abstract-Rewriting.Abstract_Rewriting
First_Order_Terms.Subterm_and_Context
Matrix.Utility
Polynomial_Factorization.Missing_List
Regular_Tree_Relations.Term_Context
Regular_Tree_Relations.Basic_Utils
Regular_Tree_Relations.Ground_Terms
Regular_Tree_Relations.FSet_Utils
Utils
Multihole_Context
Regular_Tree_Relations.Ground_Ctxt
Ground_MCtxt
Bot_Terms
Saturation
Rewriting
Regular_Tree_Relations.Tree_Automata
Regular_Tree_Relations.Tree_Automata_Det
Regular_Tree_Relations.Tree_Automata_Complement
Regular_Tree_Relations.Ground_Closure
Regular_Tree_Relations.GTT
Regular_Tree_Relations.GTT_Compose
Regular_Tree_Relations.Pair_Automaton
LV_to_GTT
NF
Tree_Automata_Derivation_Split
TA_Clousure_Const
Deriving.Generator_Aux
File ‹bnf_access.ML›
File ‹generator_aux.ML›
Deriving.Derive_Manager
File ‹derive_manager.ML›
Deriving.Comparator
Deriving.Comparator_Generator
File ‹comparator_generator.ML›
Deriving.Compare
File ‹compare_code.ML›
Deriving.Compare_Generator
File ‹compare_generator.ML›
Deriving.Compare_Instances
Containers.Containers_Auxiliary
Containers.List_Fusion
Containers.Lexicographic_Order
Containers.Extend_Partial_Order
Containers.Set_Linorder
Containers.Containers_Generator
File ‹containers_generator.ML›
Containers.Collection_Order
File ‹ccompare_generator.ML›
Deriving.Equality_Generator
File ‹equality_generator.ML›
Deriving.Equality_Instances
Containers.Collection_Eq
File ‹ceq_generator.ML›
Containers.Collection_Enum
File ‹cenum_generator.ML›
Containers.Equal
Containers.DList_Set
Containers.RBT_ext
Deriving.RBT_Comparator_Impl
Containers.RBT_Mapping2
Containers.RBT_Set2
Containers.Closure_Set
Containers.Set_Impl
File ‹set_impl_generator.ML›
Containers.AssocList
Containers.Mapping_Impl
File ‹mapping_impl_generator.ML›
Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl
Type_Instances_Impl
NF_Impl
Context_Extensions
FOR_Certificate
Lift_Root_Step
Regular_Tree_Relations.RRn_Automata
Context_RR2
GTT_RRn
FOL-Fitting.FOL_Fitting
FOL_Extra
FOR_Semantics
First_Order_Terms.Option_Monad
Regular_Tree_Relations.GTT_Transitive_Closure
Regular_Tree_Relations.AGTT
Regular_Tree_Relations.Tree_Automata_Pumping
Regular_Tree_Relations.RR2_Infinite
Regular_Tree_Relations.RR2_Infinite_Q_infinity
FOR_Check
Regular_Tree_Relations.Horn_Inference
Regular_Tree_Relations.Horn_Fset
Regular_Tree_Relations.Tree_Automata_Abstract_Impl
Containers.Map_To_Mapping
Containers.Containers
Regular_Tree_Relations.Tree_Automata_Impl
Regular_Tree_Relations.Regular_Relation_Abstract_Impl
Regular_Tree_Relations.Regular_Relation_Impl
FOR_Check_Impl