Definitions hol list 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
bchooseDef @x:'ap(x) == @x:'ap(x)
Thm* 'a:S, p:('a). (@x:'ap(x))  'a
bifDef bif(bbx.x(bx); by.y(by)) == if b x(*) else y(x.x) fi
Thm* A:Type, b:x:(bA), y:((b)A). bif(bbx.x(bx); by.y(by))  A
int_segDef {i..j} == {k:i  k < j }
Thm* m,n:. {m..n Type
lt_intDef i<j == if i<j true ; false fi
Thm* i,j:. (i<j 
natDef  == {i:| 0i }
Thm*   Type
Thm*   S
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}
tlambdaDef (x:Tb(x))(x) == b(x)

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

Definitions hol list 1 Sections HOLlib Doc