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.
rel_expDef R^n == if n=0 x,yx = y  T else x,yz:T. (x R z) & (z R^n-1 y) fi
Def (recursive)
Thm* n:T:Type, R:(TTProp). R^n  TTProp
transDef Trans x,y:TE(x;y) == a,b,c:TE(a;b E(b;c E(a;c)
Thm* T:Type, E:(TTProp). (Trans x,y:TE(x,y))  Prop

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

Definitions mb nat Sections MarkB generic Doc