1\DOC 2 3\TYPE {COMB2_CONV : conv * conv -> conv} 4 5\SYNOPSIS 6Applies two conversions to an application's subterms. 7 8\KEYWORDS 9rewriting. 10 11\DESCRIBE 12 13A call to {COMB2_CONV(c1,c2) t}, when {t} is an application term of 14the form {f x}, causes conversion {c1} to be applied to term {f}, and 15conversion {c2} to be applied to term {x}. If the results of these 16calls are theorems of the form {|- f = f���} and {|- x = x���}, then the 17result of the call to {COMB2_CONV} is the theorem {|- f x = f��� x���}. 18 19If one of the two sub-calls raises the {UNCHANGED} exception, then the 20result of that call is taken to be the reflexive theorem ({|- x = x} 21if {c2} raises the exception, for example). If both conversions raise 22the {UNCHANGED} exception, then so too does {COMB2_CONV(c1,c2) t}. 23 24\FAILURE 25Fails if the term is not a combination term, or if either conversion fails when applied to the respective sub-terms. 26 27\EXAMPLE 28{ 29> COMB2_CONV (ALL_CONV, numLib.REDUCE_CONV) ``f (10 * 3)``; 30<<HOL message: inventing new type variable names: 'a>> 31val it = |- f (10 * 3) = f 30 : thm 32} 33 34\SEEALSO 35Conv.ABS_CONV, Conv.COMB_CONV, Conv.FORK_CONV, Conv.RAND_CONV, Conv.RATOR_CONV. 36 37\ENDDOC 38