1\DOC DISJ1_TAC
2
3\TYPE {DISJ1_TAC : tactic}
4
5\SYNOPSIS
6Selects the left disjunct of a disjunctive goal.
7
8\KEYWORDS
9tactic, disjunction.
10
11\DESCRIBE
12{
13   A ?- t1 \/ t2
14  ===============  DISJ1_TAC
15     A ?- t1
16}
17
18
19\FAILURE
20Fails if the goal is not a disjunction.
21
22\SEEALSO
23Thm.DISJ1, Thm.DISJ2, Tactic.DISJ2_TAC.
24\ENDDOC
25