Context_Notation

Typing

Term_Typing

Generic_Context

Parallel_Induct

IsaFoR_Ground_Term

IsaFoR_Ground_Context

Ground_Term_Typing

Nonground_Term

Multiset_Extra

Multiset_Grounding_Lifting

Nonground_Clause_Generic

Selection_Function

Nonground_Selection_Function

HOL_Extra

Grounded_Selection_Function

IsaFoR_Nonground_Term

Literal_Functor

Uprod_Extra

Uprod_Literal_Functor

Nonground_Clause_With_Equality

IsaFoR_Nonground_Clause_With_Equality

Nonground_Context

Context_Functor

IsaFoR_Nonground_Context

Restricted_Order

Context_Compatible_Order

Term_Order_Notation

Transitive_Closure_Extra

Ground_Term_Order

Grounded_Order

Nonground_Term_Order

Multiset_Extension

Natural_Functor_To_Multiset

Grounded_Multiset_Extension

Maximal_Literal

Term_Order_Lifting

Ground_Order_Generic

Nonground_Order_Generic

Ground_Order_With_Equality

Nonground_Order_With_Equality

Selection_Function_Select_Max

IsaFoR_KBO

Nonground_Clause

IsaFoR_Nonground_Clause

Ground_Term_Rewrite_System

Ground_Critical_Pairs

Ground_Critical_Peaks

IsaFoR_Ground_Critical_Pairs

Collect_Extra

Infinite_Variables_Per_Type

Typed_Functional_Substitution

Nonground_Term_Typing

Monomorphic_Typing

Entailment_Lifting

Fold_Extra

Nonground_Entailment

Inference_Functor

Nonground_Inference

Ground_Order

Nonground_Order

Natural_Magma_Typing_Lifting

Multiset_Typing_Lifting

Clause_Typing_Generic

Typed_Functional_Substitution_Lifting

Nonground_Typing_Generic

Clause_Typing

Nonground_Typing

Clause_Typing_With_Equality

Nonground_Typing_With_Equality

Typed_Functional_Substitution_Example

Typed_Functional_Substitution_Lifting_Example

Tiebreakers

Typed_Tiebreakers

Untyped_Calculus