Def pair == x:'a. y:'b. <x,y>

is mentioned by

Thm* 'a,'b:S. Thm* all Thm* (b:'b. all Thm* (b:'b. (a:'a. all Thm* (b:'b. (a:'a. (y:'b. all Thm* (b:'b. (a:'a. (y:'b. (x:'a. equal Thm* (b:'b. (a:'a. (y:'b. (x:'a. (equal(pair(x,y),pair(a,b)) Thm* (b:'b. (a:'a. (y:'b. (x:'a. ,and(equal(x,a),equal(y,b)))))))	[hpair_eq]
Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(snd(pair(x,y)),y)))	[hsnd_pair]
Thm* 'a,'b:S. all(x:'a. all(y:'b. equal(fst(pair(x,y)),x)))	[hfst_pair]
Thm* 'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x))	[hpair_wd]
Thm* 'c,'a,'b:S. Thm* all Thm* (f:hprod('a; 'b)  'c. all Thm* (f:hprod('a; 'b)  'c. (x:'a. all Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. equal Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. (curry(f,x,y) Thm* (f:hprod('a; 'b)  'c. (x:'a. (y:'b. ,f(pair(x,y))))))	[hcurry_def]
Thm* 'c,'a,'b:S. Thm* all Thm* (f:'a  'b  'c. all Thm* (f:'a  'b  'c. (x:'a. all Thm* (f:'a  'b  'c. (x:'a. (y:'b. equal(uncurry(f,pair(x,y)),f(x,y)))))	[huncurry_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]

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