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