Session Functional_Ordered_Resolution_Prover

Theories

• Matrix.Utility
• Polynomial_Factorization.Missing_List
• Weighted_FO_Ordered_Resolution_Prover
• Lambda_Free_RPOs.Lambda_Free_Util
• Deterministic_FO_Ordered_Resolution_Prover
• 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
• Deriving.Equality_Generator
  • File ‹equality_generator.ML›
• Deriving.Equality_Instances
• Word_Lib.More_Arithmetic
• Word_Lib.More_Divides
• Word_Lib.More_Bit_Ring
• Word_Lib.More_Word
• Word_Lib.Bit_Shifts_Infix_Syntax
• Word_Lib.Most_significant_bit
• Word_Lib.Least_significant_bit
• Word_Lib.Generic_set_bit
• Word_Lib.Bit_Comprehension
• Word_Lib.Signed_Division_Word
• Native_Word.Code_Target_Word_Base
• Native_Word.Word_Type_Copies
• Native_Word.Code_Int_Integer_Conversion
• Native_Word.Code_Target_Integer_Bit
• Native_Word.Uint32
• Collections.HashCode
• Deriving.Hash_Generator
  • File ‹hash_generator.ML›
• Deriving.Hash_Instances
• Deriving.Countable_Generator
• Deriving.Derive
• First_Order_Terms.Term
• First_Order_Terms.Unifiers
• First_Order_Terms.Term_Pair_Multiset
• 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.Abstract_Unification
• First_Order_Terms.Option_Monad
• Fresh_Identifiers.Fresh
• First_Order_Terms.Renaming2
• First_Order_Terms.Unification
• First_Order_Terms.Fun_More
• First_Order_Terms.Transitive_Closure_More
• First_Order_Terms.Seq_More
• First_Order_Terms.Subsumption
• HOL-Cardinals.Order_Union
• HOL-Cardinals.Wellorder_Extension
• Open_Induction.Restricted_Predicates
• Abstract-Rewriting.Relative_Rewriting
• Knuth_Bendix_Order.Order_Pair
• Knuth_Bendix_Order.Lexicographic_Extension
• First_Order_Terms.Subterm_and_Context
• Knuth_Bendix_Order.KBO
• IsaFoR_Term
• First_Order_Terms.Abstract_Matching
• First_Order_Terms.Matching
• Executable_Subsumption
• Show.Show
  • File ‹show_generator.ML›
• Show.Show_Instances
• Executable_FO_Ordered_Resolution_Prover