Definitions hol sum 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
houtlDef outl == u:'a+'b. InjCase(uxx, arb('a))
Thm* 'a,'b:S. outl  (hsum('a'b 'a)
hsumDef hsum('a'b) == 'a+'b
Thm* 'a,'b:S. hsum('a'b S
islDef isl(x) == InjCase(xy. truez. false)
Thm* A,B:Type, x:A+B. isl(x 
outlDef outl(x) == InjCase(xyyz. "???")
Thm* A,B:Type, x:A+B. isl(x outl(x A
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}

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

Definitions hol sum Sections HOLlib Doc