menu

Return to entry

Generic_Term
Context_Notation
Generic_Context
Generic_Term_Context
Ground_Term_Rewrite_System
Parallel_Induct
Parallel_Rewrite
Ground_Critical_Pairs
Typing
Term_Typing
IsaFoR_Abstract_Context
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
Infinite_Variables
Restricted_Order
Tiebreakers
Typed_Tiebreakers
Collect_Extra
Infinite_Variables_Per_Type
Typed_Substitution
Nonground_Context
Nonground_Term_Typing
Natural_Magma_Typing_Lifting
Multiset_Typing_Lifting
Literal_Functor
Clause_Typing_Generic
Typed_Substitution_Lifting
Nonground_Typing_Generic
Untyped_Calculus
IsaFoR_Nonground_Term
Uprod_Extra
Uprod_Literal_Functor
Nonground_Clause_With_Equality
IsaFoR_Nonground_Clause_With_Equality
Context_Functor
IsaFoR_Nonground_Context
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
IsaFoR_Ground_Term_Compatibility
Entailment_Lifting
Fold_Extra
Nonground_Entailment
Inference_Functor
Nonground_Inference
Ground_Order
Nonground_Order
Clause_Typing
Nonground_Typing
Weak_Typing
Weak_Typing_Magma
Weak_Typing_Multiset
Clause_Typing_With_Equality
Weakly_Typed_Substitution
Nonground_Typing_With_Equality
Abstract_Context
Polymorphic_Ground_Term
Polymorphic_Ground_Context
Typed_IMGU
Monomorphic_Typing_Compatibility
Monomorphic_Typing
Sorted_Terms_Typing
Typed_Substitution_Example
Typed_Substitution_Lifting_Example

First_Order_Clause.Weakly_Typed_Substitution

HTML Presentation