----------------------------------------------------------------------
RAND_CONV                                                       (Conv)
----------------------------------------------------------------------
RAND_CONV : (conv -> conv)

SYNOPSIS
Applies a conversion to the operand of an application.

KEYWORDS
conversional.

DESCRIBE
If {c} is a conversion that maps a term {"t2"} to the theorem {|- t2 = t2'},
then the conversion {RAND_CONV c} maps applications of the form {"t1 t2"} to
theorems of the form:

   |- (t1 t2) = (t1 t2')

That is, {RAND_CONV c "t1 t2"} applies {c} to the operand of the
application {"t1 t2"}.

FAILURE
{RAND_CONV c tm} fails if {tm} is not an application or if {tm} has the form
{"t1 t2"} but the conversion {c} fails when applied to the term {t2}. The
function returned by {RAND_CONV c} may also fail if the ML function
{c:term->thm} is not, in fact, a conversion (i.e. a function that maps a term
{t} to a theorem {|- t = t'}).

EXAMPLE

- RAND_CONV numLib.num_CONV (Term `SUC 2`);
> val it = |- SUC 2 = SUC(SUC 1) : thm




SEEALSO
Conv.ABS_CONV, Conv.BINOP_CONV, Conv.LAND_CONV, Conv.RATOR_CONV,
Conv.SUB_CONV, Conv.RHS_CONV.

----------------------------------------------------------------------