1\DOC CONJ_ASM2_TAC 2 3\TYPE {CONJ_ASM2_TAC : tactic} 4 5\SYNOPSIS 6Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming 7the second, then prove the second conjunct. 8 9\KEYWORDS 10tactic, conjunction. 11 12\DESCRIBE 13When applied to a goal {A ?- t1 /\ t2}, the tactic {CONJ_ASM2_TAC} reduces it 14to two subgoals corresponding to the two conjuncts, assuming the first to 15prove the second. 16{ 17 A ?- t1 /\ t2 18 ========================== CONJ_ASM2_TAC 19 A u {t2} ?- t1 A ?- t2 20} 21 22 23\FAILURE 24Fails unless the conclusion of the goal is a conjunction. 25 26\SEEALSO 27Tactic.CONJ_ASM1_TAC, Tactic.CONJ_TAC, Tactical.USE_SG_THEN. 28\ENDDOC 29