BINOP_CONV : conv -> conv
STRUCTURE
SYNOPSIS
Applies a conversion to both arguments of a binary operator.
LIBRARY
DESCRIPTION
If c is a conversion that when applied to t1 returns the theorem |- t1 = t1' and when applied to t2 returns the theorem |- t2 = t2', then BINOP_CONV c (Term`f t1 t2`) will return the theorem
   |- f t1 t2 = f t1' t2'

FAILURE
BINOP_CONV c t will fail if t is not of the general form f t1 t2, or if c fails when applied to either t1 or t2, or if c fails to return theorems of the form |- t1 = t1' and |- t2 = t2' when applied to those arguments. (The latter case would imply that c wasn’t a conversion at all.)
EXAMPLE
- BINOP_CONV REDUCE_CONV (Term`3 * 4 + 6 * 7`);
> val it = |- 3 * 4 + 6 * 7 = 12 + 42 : thm

SEEALSO
HOL  Kananaskis-14