CONJ_TAC : tactic
STRUCTURE
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
Fails unless the conclusion of the goal is a conjunction.
SEEALSO
STRIP_TAC
HOL  Kananaskis-14