\DOC CONJ_TAC

\TYPE {CONJ_TAC : tactic}

\SYNOPSIS
Reduces a conjunctive goal to two separate subgoals.

\KEYWORDS
tactic, conjunction.

\DESCRIBE
When applied to a goal {A ?- t1 /\ t2}, the tactic {CONJ_TAC} reduces it to the
two subgoals corresponding to each conjunct separately.
{
       A ?- t1 /\ t2
   ======================  CONJ_TAC
    A ?- t1      A ?- t2
}


\FAILURE
Fails unless the conclusion of the goal is a conjunction.

\SEEALSO
Tactic.STRIP_TAC.
\ENDDOC