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