# [isabelle] Ordered Pair Definition

Deal all
I'm looking for the essential definition of ordered pair in Isabelle/HOL as
I found it in Isabelle/ZF but I need it on HOL and I found some theories in
Isabelle/HOL like : Product_Type,Relation, Fun_Def, Function_Order,
Relators, BNF_Def, Wellfounded and many other theories. My question is
where I can find the essential definition of ordered pair product as a
function. I've seen the product definition in Product_Type theory but I
still can't find the definition of ordered pair as in set theory (as a
function).
So, is there and function or definition says that the ('a x'b)set is a
function or relation of AXB where for pair (a,b):C a:A and b:B and C is
('a x'b)set.
Cheers
Jasim

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*