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

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

Definitions hol bool Sections HOLlib Doc