1\DOC ABS_CONV
2
3\TYPE {ABS_CONV : conv -> conv}
4
5\SYNOPSIS
6Applies a conversion to the body of an abstraction.
7
8\KEYWORDS
9conversional, abstraction.
10
11\DESCRIBE
12If {c} is a conversion that maps a term {tm} to the theorem {|- tm = tm'},
13then the conversion {ABS_CONV c} maps abstractions of the form {\x.tm} to
14theorems of the form:
15{
16   |- (\x.tm) = (\x.tm')
17}
18That is, {ABS_CONV c (\x.t)} applies {c} to the body of the
19abstraction {\x.t}.
20
21\FAILURE
22{ABS_CONV c tm} fails if {tm} is not an abstraction or if {tm} has the form
23{\x.t} but the conversion {c} fails when applied to the term {t}. The
24function returned by {ABS_CONV c} may also fail if the ML function
25{c:term->thm} is not, in fact, a conversion (i.e. a function that maps a term
26{M} to a theorem {|- M = N}).
27
28\EXAMPLE
29{
30- ABS_CONV SYM_CONV (Term `\x. 1 = x`)
31> val it = |- (\x. 1 = x) = (\x. x = 1) : thm
32}
33
34
35\SEEALSO
36Conv.RAND_CONV, Conv.RATOR_CONV, Conv.SUB_CONV,
37Conv.BINDER_CONV, Conv.QUANT_CONV,
38Conv.STRIP_BINDER_CONV, Conv.STRIP_QUANT_CONV.
39
40\ENDDOC
41