Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
double_sumDef sum(f(x;y) | x < ny < m) == sum(sum(f(x;y) | y < m) | x < n)
Thm* n,m:f:(nm). sum(f(x,y) | x < ny < m 
int_segDef {i..j} == {k:i  k < j }
Thm* m,n:. {m..n Type
natDef  == {i:| 0i }
Thm*   Type

About:
intnatural_numbersetfunctionuniversememberall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb nat Sections MarkB generic Doc