Session First_Order_Terms

Theories

• Transitive_Closure_More
• Fresh_Identifiers.Fresh
• Renaming2
• Lists_are_Infinite
• Renaming2_String
• Seq_More
• Fun_More
• Option_Monad
• Term
• Term_Pair_Multiset
• Abstract_Matching
• Unifiers
• Abstract_Unification
• Unification
• Matching
• Unification_String
• Subsumption
• Subterm_and_Context