dest_disj : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Term destructor for disjunctions.
DESCRIPTION
If
M
is a term having the form
t1 \/ t2
, then
dest_disj M
returns
(t1,t2)
.
FAILURE
Fails if
M
is not a disjunction.
SEEALSO
mk_disj
,
is_disj
,
strip_disj
,
list_mk_disj
HOL
Kananaskis-14