Def is_pair == p:'a'b. x:'a. y:'b. (p = (mk_pair(x,y)))

is mentioned by

Thm* 'a,'b:S. Thm* exists Thm* (rep:hprod('a; 'b)  'a  'b  hbool. type_definition(is_pair,rep))	[hprod_ty_def]
Thm* 'a,'b:S. Thm* equal Thm* (rep_prod Thm* ,select Thm* ,(rep:hprod('a; 'b) Thm* ,( 'a Thm* ,( 'b Thm* ,( hbool. and Thm* ,( hbool. (all Thm* ,( hbool. ((p':hprod('a; 'b). all Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). implies Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (equal Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ((rep(p') Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (,rep(p'')) Thm* ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ,equal(p',p'')))) Thm* ,( hbool. ,all Thm* ,( hbool. ,(p:'a  'b  hbool. equal Thm* ,( hbool. ,(p:'a  'b  hbool. (is_pair(p) Thm* ,( hbool. ,(p:'a  'b  hbool. ,exists Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). equal Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). (p Thm* ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). ,rep(p'))))))))	[hrep_prod_wd]
Thm* 'a,'b:S. Thm* all Thm* (p:'a  'b  hbool. equal Thm* (p:'a  'b  hbool. (is_pair(p) Thm* (p:'a  'b  hbool. ,exists Thm* (p:'a  'b  hbool. ,(x:'a. exists(y:'b. equal(p,mk_pair(x,y))))))	[his_pair_def]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html