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))  
bandDef pq == if p q else false fi
Thm* p,q:. (pq 
bimpliesDef pq == p  q
Thm* p,q:pq  
tlambdaDef (x:Tb(x))(x) == b(x)

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

Definitions hol bool Sections HOLlib Doc