Definitions union Sections StandardLIB 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
bnotDef b == if b false else true fi
Thm* b:b  
islDef isl(x) == InjCase(xy. truez. false)
Thm* A,B:Type, x:A+B. isl(x 
outrDef outr(x) == InjCase(xy. "???"; zz)
Thm* A,B:Type, x:A+Bisl(x outr(x B

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

Definitions union Sections StandardLIB Doc