Session FO_Theory_Rewriting

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
• 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.Shows_Literal
• First_Order_Terms.Position
• Matrix.Utility
• Polynomial_Factorization.Missing_List
• First_Order_Terms.Unifiers
• First_Order_Terms.Term_Pair_Multiset
• First_Order_Terms.Abstract_Unification
• First_Order_Terms.Option_Monad
• Fresh_Identifiers.Fresh
• First_Order_Terms.Renaming2
• First_Order_Terms.Fun_More2
• First_Order_Terms.Unification
• First_Order_Terms.Term_More
• Regular_Tree_Relations.Term_Context
• Regular_Tree_Relations.Basic_Utils
• Regular_Tree_Relations.Ground_Terms
• Regular_Tree_Relations.FSet_Utils
• Certification_Monads.Error_Syntax
• Certification_Monads.Error_Monad
• Certification_Monads.Check_Monad
• 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
• Deriving.Compare_Order_Instances
• First_Order_Terms.Term_Impl
• Utils
• Abstract-Rewriting.Relative_Rewriting
• Abstract-Rewriting.Relation_Closure
• First_Order_Rewriting.Trs
• First_Order_Rewriting.FOR_Preliminaries
• First_Order_Rewriting.SubList
• First_Order_Rewriting.Multihole_Context
• Multihole_Context_More
• Regular_Tree_Relations.Ground_Ctxt
• Ground_MCtxt
• Bot_Terms
• Saturation
• First_Order_Rewriting.Parallel_Rewriting
• 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
• 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_Extra
• FOR_Semantics
• 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