----------------------------------------------------------------------
FORK_CONV                                                       (Conv)
----------------------------------------------------------------------
FORK_CONV : (conv * conv) -> conv

SYNOPSIS
Applies a pair of conversions to the arguments of a binary operator.

KEYWORDS
conversional.

DESCRIBE
If the conversion {c1} maps a term {t1} to the theorem {|- t1 = t1'},
and the conversion {c2} maps {t2} to {|- t2 = t2'}, then the
conversion {FORK_CONV (c1,c2)} maps terms of the form {f t1 t2} to
theorems of the form {|- f t1 t2 = f t1' t2'}.

FAILURE
{FORK_CONV (c1,c2) t} will fail if {t} is not of the general form
{f t1 t2}, or if {c1} fails when applied to {t1}, or if {c2} fails when
applied to {t2}, or if {c1} or {c2} aren’t really conversions, and
thereby fail to return appropriate equational theorems.



EXAMPLE

- FORK_CONV (BETA_CONV,REDUCE_CONV) (Term`(\x. x + 1)y * (10 DIV 3)`);
> val it = |- (\x. x + 1) y * (10 DIV 3) = (y + 1) * 3 : thm


SEEALSO
Conv.BINOP_CONV, Conv.LAND_CONV, Conv.RAND_CONV, Conv.RATOR_CONV,
numLib.REDUCE_CONV.

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