----------------------------------------------------------------------
CONJ_ASM2_TAC                                                 (Tactic)
----------------------------------------------------------------------
CONJ_ASM2_TAC : tactic

SYNOPSIS
Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming
the second, then prove the second conjunct.

KEYWORDS
tactic, conjunction.

DESCRIBE
When applied to a goal {A ?- t1 /\ t2}, the tactic {CONJ_ASM2_TAC} reduces it
to two subgoals corresponding to the two conjuncts, assuming the first to
prove the second.

         A ?- t1 /\ t2
   ==========================  CONJ_ASM2_TAC
    A u {t2} ?- t1   A ?- t2




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

SEEALSO
Tactic.CONJ_ASM1_TAC, Tactic.CONJ_TAC, Tactical.USE_SG_THEN.

----------------------------------------------------------------------