Session Unordered_Resolution
View
theory dependencies
Theories
Infinite_Set
Regular_Set
Regular_Exp
NDerivative
While_Combinator
Equivalence_Checking
Relation_Interpretation
Regexp_Method
Seq
Abstract_Rewriting
Generator_Aux
Derive_Manager
Show
Show_Instances
Position
Utility
Logic_Util
Adhoc_Overloading
Monad_Syntax
Missing_List
List_Util
Relative_Rewriting
Util
Multiset
Relations
Multiset2
Sharp_Syntax
Term
Unifiers
Term_Pair_Multiset
Abstract_Unification
Option_Monad
Decomp
Unification
Old_Datatype
Nat_Bijection
Countable
Countable_Set
TermsAndLiterals
Tree
Resolution
Unify
Completeness
Examples