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