FORK_CONV : (conv * conv) -> conv
STRUCTURE
SYNOPSIS
Applies a pair of conversions to the arguments of a binary operator.
DESCRIPTION
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
HOL  Trindemossen-1