Transitive_Closure_Extra

Abstract_Rewriting_Extra

Term_Rewrite_System

Ground_Critical_Pairs

Multiset_Extra

Uprod_Extra

HOL_Extra

Relation_Extra

Clausal_Calculus_Extra

Ground_Term_Extra

Ground_Ctxt_Extra

Ground_Clause

Selection_Function

Term_Ordering_Lifting

Ground_Ordering

Ground_Type_System

Ground_Superposition

Ground_Superposition_Completeness

Variable_Substitution

First_Order_Clause

Fun_Extra

First_Order_Type_System

First_Order_Select

First_Order_Ordering

First_Order_Superposition

Grounded_First_Order_Superposition

First_Order_Superposition_Completeness

IsaFoR_Term_Copy

First_Order_Superposition_Example

First_Order_Superposition_Soundness

Ground_Superposition_Soundness

Ground_Superposition_Welltypedness_Preservation