Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
ballDef x:TP(x) == (x:TP(x))
Thm* T:Type, P:(T). (x:TP(x))  
assertDef b == if b True else False fi
Thm* b:b  Prop
bequalDef x = y == (x = y  T)
Thm* T:Type, x,y:T. (x = y 
bimpliesDef pq == p  q
Thm* p,q:pq  
borDef p  q == if p true else q fi
Thm* p,q:. (p  q 

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

Definitions hol bool Sections HOLlib Doc