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:That is, ABS_CONV c "\p.t" applies p to the body of the paired abstraction "\p.t".
|- (\p.t) = (\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-14