Session Unordered_Resolution

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