WhoCites Definitions hol arithmetic 3 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites bnot?
bnotDef b == if b false else true fi
Thm* b:b  
btrueDef true == inl()
Thm* true  
bfalseDef false == inr()
Thm* false  
ifthenelseDef if b t else f fi == InjCase(b ; tf)
Thm* b:A:Type, p,q:A. if b p else q fi  A

Syntax:b has structure: bnot(b)

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

WhoCites Definitions hol arithmetic 3 Sections HOLlib Doc