----------------------------------------------------------------------
RHS_CONV                                                        (Conv)
----------------------------------------------------------------------
RHS_CONV : conv -> conv

SYNOPSIS
Applies a conversion to the right-hand argument of an equality.

KEYWORDS
conversional

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

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




FAILURE
{RHS_CONV c tm} fails if {tm} is not an an equality {t1 = t2},
or if {tm} has this form 
but the conversion {c} fails when applied to the term {t2}. The
function returned by {RHS_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

- RHS_CONV REDUCE_CONV (Term`7 = (3 + 5)`);
> val it = |- (7 = (3 + 5)) = (7 = 8) : thm


COMMENTS
{RAND_CONV} is similar, but works for any binary operator

SEEALSO
Conv.BINOP_CONV, Conv.LHS_CONV, numLib.REDUCE_CONV, Conv.RAND_CONV.

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