----------------------------------------------------------------------
CONJ_ASM1_TAC                                                 (Tactic)
----------------------------------------------------------------------
CONJ_ASM1_TAC : tactic

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

KEYWORDS
tactic, conjunction.

DESCRIBE
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
Tactic.CONJ_ASM2_TAC, Tactic.CONJ_TAC, Tactical.USE_SG_THEN.

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