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