1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
\DOC COMB2_CONV
\TYPE {COMB2_CONV : (term -> thm) -> (term -> thm) -> term -> thm}
\SYNOPSIS
Applies two conversions to the two sides of an application.
\DESCRIBE
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
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.
\COMMENTS
The special case when the two conversions are the same is more briefly achieved
using {COMB_CONV}.
\SEEALSO
BINOP_CONV, BINOP2_CONV, COMB_CONV, LAND_CONV, RAND_CONV, RATOR_CONV
\ENDDOC
|
