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