GABS_CONV : conv -> term -> thm

SYNOPSIS
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)

SEE ALSO
ABS_CONV, RAND_CONV, RATOR_CONV, SUB_CONV.