mk_pair : term * term -> term
STRUCTURE
pairSyntax
SYNOPSIS
Constructs object-level pair from a pair of terms.
DESCRIPTION
mk_pair (t1,t2)
returns
(t1,t2)
.
FAILURE
Never fails.
SEEALSO
dest_pair
,
is_pair
,
list_mk_pair
HOL
Kananaskis-14