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