Ground_Term_Extra

Ground_Context

Multiset_Extra

Uprod_Extra

Ground_Clause

Typing

Natural_Magma_Typing_Lifting

Multiset_Typing_Lifting

Clausal_Calculus_Extra

Clause_Typing

Context_Extra

Term_Typing

Ground_Typing

Nonground_Term

Nonground_Context

Multiset_Grounding_Lifting

Nonground_Clause

Selection_Function

Nonground_Selection_Function

Infinite_Variables_Per_Type

Collect_Extra

Typed_Functional_Substitution

Functional_Substitution_Typing

Typed_Functional_Substitution_Lifting

Functional_Substitution_Typing_Lifting

Nonground_Term_Typing

Nonground_Typing

HOL_Extra

Grounded_Selection_Function

Term_Rewrite_System

Entailment_Lifting

Fold_Extra

Nonground_Entailment

Nonground_Inference

Restricted_Order

Context_Compatible_Order

Term_Order_Notation

Transitive_Closure_Extra

Ground_Term_Order

Grounded_Order

Multiset_Extension

Grounded_Multiset_Extension

Maximal_Literal

Term_Order_Lifting

Ground_Order

Nonground_Term_Order

Nonground_Order

Typed_Functional_Substitution_Example

Typed_Functional_Substitution_Lifting_Example