dest_pair : term -> term * term
STRUCTURE
pairSyntax
SYNOPSIS
Breaks apart a pair into two separate terms.
LIBRARY
pair
DESCRIPTION
dest_pair
is a term destructor for pairs: if
M
is a term of the form
(t1,t2)
, then
dest_pair M
returns
(t1,t2)
.
FAILURE
Fails if
M
is not a pair.
SEEALSO
mk_pair
,
is_pair
,
strip_pair
HOL
Kananaskis-10