1\DOC CONJUNCTS_THEN2 2 3\TYPE {CONJUNCTS_THEN2 : (thm_tactic -> thm_tactical)} 4 5\SYNOPSIS 6Applies two theorem-tactics to the corresponding conjuncts of a theorem. 7 8\KEYWORDS 9theorem-tactic, conjunction. 10 11\DESCRIBE 12{CONJUNCTS_THEN2} takes two theorem-tactics, {f1} and {f2}, and a theorem {t} 13whose conclusion must be a conjunction. {CONJUNCTS_THEN2} breaks {t} into two 14new theorems, {t1} and {t2} which are {CONJUNCT1} and {CONJUNCT2} of {t} 15respectively, and then returns the tactic {f1 t1 THEN f2 t2}. Thus 16{ 17 CONJUNCTS_THEN2 f1 f2 (A |- l /\ r) = f1 (A |- l) THEN f2 (A |- r) 18} 19so if 20{ 21 A1 ?- t1 A2 ?- t2 22 ========== f1 (A |- l) ========== f2 (A |- r) 23 A2 ?- t2 A3 ?- t3 24} 25then 26{ 27 A1 ?- t1 28 ========== CONJUNCTS_THEN2 f1 f2 (A |- l /\ r) 29 A3 ?- t3 30} 31 32 33\FAILURE 34{CONJUNCTS_THEN f} will fail if applied to a theorem whose conclusion is not a 35conjunction. 36 37\COMMENTS 38The system shows the type as {(thm_tactic -> thm_tactical)}. 39 40\USES 41The construction of complex {tactical}s like {CONJUNCTS_THEN}. 42 43\SEEALSO 44Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJUNCTS, Tactic.CONJ_TAC, Thm_cont.CONJUNCTS_THEN2, Thm_cont.STRIP_THM_THEN. 45\ENDDOC 46