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

is mentioned by

Thm* 'a,'b:S. Thm* all Thm* (p:hprod('a; 'b). equal Thm* (p:hprod('a; 'b). (snd(p) Thm* (p:hprod('a; 'b). ,select Thm* (p:hprod('a; 'b). ,(y:'b. exists Thm* (p:hprod('a; 'b). ,(y:'b. (x:'a. equal(mk_pair(x,y),rep_prod(p))))))	[hsnd_def]
Thm* 'a,'b:S. Thm* all Thm* (p:hprod('a; 'b). equal Thm* (p:hprod('a; 'b). (fst(p) Thm* (p:hprod('a; 'b). ,select Thm* (p:hprod('a; 'b). ,(x:'a. exists Thm* (p:hprod('a; 'b). ,(x:'a. (y:'b. equal(mk_pair(x,y),rep_prod(p))))))	[hfst_def]
Thm* 'a,'b:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (y:'b. equal Thm* (x:'a. (y:'b. (pair(x,y) Thm* (x:'a. (y:'b. ,select Thm* (x:'a. (y:'b. ,(p:hprod('a; 'b). equal(rep_prod(p),mk_pair(x,y))))))	[hcomma_def]
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]
Thm* 'a,'b:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (y:'b. equal Thm* (x:'a. (y:'b. (mk_pair(x,y) Thm* (x:'a. (y:'b. ,a:'a. b:'b. and(equal(a,x),equal(b,y)))))	[hmk_pair_def]
Def rep_prod == p:'a'b. mk_pair(1of(p),2of(p))	[hrep_prod]
Def is_pair == p:'a'b. x:'a. y:'b. (p = (mk_pair(x,y)))	[his_pair]

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