COMB2_CONV : (term -> thm) -> (term -> thm) -> term -> thm

- SYNOPSIS
- Applies two conversions to the two sides of an application.
- DESCRIPTION
- 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