Applies a conversion to the body of a generalized abstraction.
DESCRIPTION
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:
|- (\vs. t) = (\vs. t')
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.
EXAMPLE
# 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)