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)