DISJ2_TAC : tactic
STRUCTURE
Tactic
SYNOPSIS
Selects the right disjunct of a disjunctive goal.
DESCRIPTION
A ?- t1 \/ t2 =============== DISJ2_TAC A ?- t2
FAILURE
Fails if the goal is not a disjunction.
SEEALSO
DISJ1
,
DISJ1_TAC
,
DISJ2
HOL
Trindemossen-1