ABS_CONV
Conv.ABS_CONV : conv -> conv
Applies a conversion to the body of an abstraction.
If c is a conversion that maps a term tm to the theorem
|- tm = tm', then the conversion ABS_CONV c maps abstractions of the
form \x.tm to theorems of the form:
|- (\x.tm) = (\x.tm')
That is, ABS_CONV c (\x.t) applies c to the body of the abstraction
\x.t.
Failure
ABS_CONV c tm fails if tm is not an abstraction or if tm has the
form \x.t but the conversion c fails when applied to the term t.
The function returned by ABS_CONV c may also fail if the ML function
c:term->thm is not, in fact, a conversion (i.e. a function that maps a
term M to a theorem |- M = N).
Example
> ABS_CONV SYM_CONV (Term `\x. 1 = x`)
val it = ⊢ (λx. 1 = x) = (λx. x = 1): thm
See also
Conv.RAND_CONV,
Conv.RATOR_CONV,
Conv.SUB_CONV,
Conv.BINDER_CONV,
Conv.QUANT_CONV,
Conv.STRIP_BINDER_CONV,
Conv.STRIP_QUANT_CONV