dest_pair : term -> term * term
STRUCTURE
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
HOL  Trindemossen-1