PABS_CONV : conv -> conv
STRUCTURE
LIBRARY
pair
SYNOPSIS
Applies a conversion to the body of a paired abstraction.
DESCRIPTION
If c is a conversion that maps a term t to the theorem |- t = t', then the conversion PABS_CONV c maps abstractions of the form \p.t to theorems of the form:
   |- (\p.t) = (\p.t')
That is, ABS_CONV c "\p.t" applies p to the body of the paired abstraction "\p.t".
FAILURE
PABS_CONV c tm fails if tm is not a paired abstraction or if tm has the form "\p.t" but the conversion c fails when applied to the term t. The function returned by ABS_CONV p may also fail if the ML function c:term->thm is not, in fact, a conversion (i.e. a function that maps a term t to a theorem |- t = t').
EXAMPLE
- PABS_CONV SYM_CONV (Term `\(x,y). (1,2) = (x,y)`);
> val it = |- (\(x,y). (1,2) = (x,y)) = (\(x,y). (x,y) = (1,2)) : thm

SEEALSO
HOL  Kananaskis-13