Definitions hol pair Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
hmk_pairDef mk_pair == x:'ay:'ba:'ab:'b. (a = x)(b = y)
Thm* 'a,'b:S. mk_pair  ('a  'b  'a  'b  hbool)
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 
hboolDef hbool == 
Thm* hbool  S
hfunDef 'a  'b == 'a'b
Thm* 'a,'b:S. ('a  'b S
stypeDef S == {T:Type| x:T. True }
Thm* S  Type{2}
tlambdaDef (x:Tb(x))(x) == b(x)

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

Definitions hol pair Sections HOLlib Doc