type ('a,'b) subst
STRUCTURE
SYNOPSIS
Type abbreviation for substitutions.
DESCRIPTION
The type ('a,'b) subst abbreviates the type {redex,residue} list, in which redex has type 'a and residue has type 'b. Usually, a {redex,residue} pair in a substition is interpreted as ‘replace occurrences of redex by residue’.
COMMENTS
The different types of redex and residue components allows flexibility, as in the rule of inference SUBST, which takes a (term,thm) subst argument.
SEEALSO
HOL  Kananaskis-14