Definitions mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
eq_lnkDef a = b == eqof(IdLnkDeq)(a,b)
Thm* a,b:IdLnk. a = b  
worldDef World
Def == T:IdIdType
Def == TA:IdIdType
Def == M:IdLnkIdType
Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i)))
Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
Thm* World  Type{i'}
IdDef Id == Atom
Thm* Id  Type
assertDef b == if b True else False fi
Thm* b:b  Prop
bandDef pq == if p q else false fi
Thm* p,q:. (pq 
bnotDef b == if b false else true fi
Thm* b:b  
isrcvDef isrcv(k) == isl(k)
Thm* k:Knd. isrcv(k 
lnkDef lnk(k) == 1of(outl(k))
Thm* k:Knd. isrcv(k lnk(k IdLnk
natDef  == {i:| 0i }
Thm*   Type
notDef A == A  False
Thm* A:Prop. (A Prop
w-aDef a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)
w-isnullDef isnull(a) == isl(a)
w-kindDef kind(a) == 1of(outr(a))

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

Definitions mb event system 3 Sections EventSystems Doc