Definitions hol bool Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
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 

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

Definitions hol bool Sections HOLlib Doc