Session Resolution_FOL
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.Infinite_Set
HOL-Library.Countable_Set
TermsAndLiterals
Tree
Resolution
Completeness
Examples
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
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
HOL-Library.While_Combinator
Regular-Sets.Equivalence_Checking
Regular-Sets.Relation_Interpretation
Regular-Sets.Regexp_Method
Abstract-Rewriting.Seq
Abstract-Rewriting.Abstract_Rewriting
First_Order_Terms.Abstract_Unification
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
First_Order_Terms.Option_Monad
Fresh_Identifiers.Fresh
First_Order_Terms.Renaming2
First_Order_Terms.Unification
Unification_Theorem
Completeness_Instance