hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def curry == f:'a'b'cx:'ay:'bf(<x,y>)

is mentioned by

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]

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

hol pair Sections HOLlib Doc