----------------------------------------------------------------------
PABS_CONV                                                  (PairRules)
----------------------------------------------------------------------
PABS_CONV : conv -> conv

KEYWORDS
conversional, abstraction.

LIBRARY
pair

SYNOPSIS
Applies a conversion to the body of a paired abstraction.

DESCRIBE
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
Conv.ABS_CONV, PairRules.PSUB_CONV.

----------------------------------------------------------------------