GABS_CONV : conv -> term -> thm
Applies a conversion to the body of a generalized abstraction.
If c is a conversion that maps a term `t` to the theorem |- t = t', then
the conversion ABS_CONV c maps generalized abstractions of the form
`\vs. t` to theorems of the form:
That is, ABS_CONV c `\vs. t` applies c to the body of the
generalized abstraction `\vs. t`. It is permissible to use it on a basic
abstraction, in which case the effect is the same as ABS_CONV.
- FAILURE CONDITIONS
Fails if applied to a term that is not a generalized abstraction (or a basic
one), or if the conversion c fails when applied to the term t, or if the
theorem returned has assumptions in which one of the variables in the
abstraction varstruct is free.
# GABS_CONV SYM_CONV `\(x,y,z). x + y + z = 7`;;
val it : thm = |- (\(x,y,z). x + y + z = 7) = (\(x,y,z). 7 = x + y + z)
- SEE ALSO
ABS_CONV, RAND_CONV, RATOR_CONV, SUB_CONV.