CONJ_ASM1_TAC : tactic
STRUCTURE
SYNOPSIS
Reduces a conjunctive goal to two subgoals: prove the first conjunct, then the second assuming the first.
DESCRIPTION
When applied to a goal A ?- t1 /\ t2, the tactic CONJ_ASM1_TAC reduces it to two subgoals corresponding to the first conjunct then the second conjunct.
         A ?- t1 /\ t2
   ==========================  CONJ_ASM1_TAC
    A ?- t1   A u {t1} ?- t2

FAILURE
Fails unless the conclusion of the goal is a conjunction.
SEEALSO
HOL  Trindemossen-1