CONJ_TAC : tactic

SYNOPSIS

Reduces a conjunctive goal to two separate subgoals.

DESCRIPTION

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 CONDITIONS

Fails unless the conclusion of the goal is a conjunction.

SEE ALSO

STRIP_TAC.