1\DOC CONJ_ASM1_TAC
2
3\TYPE {CONJ_ASM1_TAC : tactic}
4
5\SYNOPSIS
6Reduces a conjunctive goal to two subgoals: prove the first conjunct, then the
7second assuming the first.
8
9\KEYWORDS
10tactic, conjunction.
11
12\DESCRIBE
13When applied to a goal {A ?- t1 /\ t2}, the tactic {CONJ_ASM1_TAC} reduces it
14to two subgoals corresponding to the first conjunct then the second conjunct.
15{
16         A ?- t1 /\ t2
17   ==========================  CONJ_ASM1_TAC
18    A ?- t1   A u {t1} ?- t2
19}
20
21
22\FAILURE
23Fails unless the conclusion of the goal is a conjunction.
24
25\SEEALSO
26Tactic.CONJ_ASM2_TAC, Tactic.CONJ_TAC, Tactical.USE_SG_THEN.
27\ENDDOC
28