1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC GABS_CONV
\TYPE {GABS_CONV : conv -> term -> thm}
\SYNOPSIS
Applies a conversion to the body of a generalized abstraction.
\DESCRIBE
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')
}
\noindent 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
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)
}
\SEEALSO
ABS_CONV, RAND_CONV, RATOR_CONV, SUB_CONV.
\ENDDOC
|
