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.
iffDef P  Q == (P  Q) & (P  Q)
Thm* A,B:Prop. (A  B Prop
natDef  == {i:| 0i }
Thm*   Type
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
rel_inverseDef R^-1(x,y) == y R x
Thm* T1,T2:Type, R:(T1T2Prop). R^-1  T2T1Prop

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

Definitions mb nat Sections MarkB generic Doc