Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
arbDef arb(T) == InjCase(lem(T); xx, "uu")
Thm* T:S. arb(T T
bandDef pq == if p q else false fi
Thm* p,q:. (pq 
bequalDef x = y == (x = y  T)
Thm* T:Type, x,y:T. (x = y 
bnotDef b == if b false else true fi
Thm* b:b  
labelDef t  ...$L == t
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}
tlambdaDef (x:Tb(x))(x) == b(x)

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

Definitions hol sum Sections HOLlib Doc