DISJ1_TAC : tactic
SYNOPSIS
Selects the left disjunct of a disjunctive goal.
DESCRIPTION
A ?- t1 \/ t2 =============== DISJ1_TAC A ?- t1
FAILURE CONDITIONS
Fails if the goal is not a disjunction.
SEE ALSO
DISJ1
,
DISJ2
,
DISJ2_TAC
.