COMB2_CONV : (term -> thm) -> (term -> thm) -> term -> thm
Applies two conversions to the two sides of an application.
If c1 and c2 are conversions such that c1 `f` returns |- f = f' and
c2 `x` returns |- x = x', then COMB2_CONV c1 c2 `f x` returns
|- f x = f' x'. That is, the conversions c1 and c2 are applied
respectively to the two immediate subterms.
- FAILURE CONDITIONS
Never fails when applied to the initial conversions. On application to the term,
it fails if either c1 or c2 does, or if either returns a theorem that is of
the wrong form.
- SEE ALSO
BINOP_CONV, COMB_CONV, LAND_CONV, RAND_CONV, RATOR_CONV