WhoCites Definitions hol arithmetic 3 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites bimplies?
bimpliesDef pq == p  q
Thm* p,q:pq  
bnotDef b == if b false else true fi
Thm* b:b  
borDef p  q == if p true else q fi
Thm* p,q:. (p  q 
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:pq has structure: bimplies(pq)

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