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