dest_conj : term -> term * term
STRUCTURE
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
HOL  Kananaskis-14