CONJ_ASM2_TAC : tactic
STRUCTURE
SYNOPSIS
Reduces a conjunctive goal to two subgoals: prove the first conjunct assuming the second, then prove the second conjunct.
DESCRIPTION
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
HOL  Trindemossen-1