dest_conj : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Term destructor for conjunctions.
DESCRIPTION
If
M
is a term
t1 /\ t2
, then
dest_conj M
returns
(t1,t2)
.
FAILURE
Fails if
M
is not a conjunction.
SEEALSO
mk_conj
,
is_conj
,
list_mk_conj
,
strip_conj
HOL
Kananaskis-14