hol
bool
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
all(
t
:hbool. or(equal(
t
,t),equal(
t
,f)))
[hbool_cases_ax]
cites the following:
Thm*
b
:
.
b
= true
b
= false
[bool_cases]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
bool
Sections
HOLlib
Doc
t:hbool. or(equal(t,t),equal(t,f)))
b:
. b = true
b = falset:hbool. or(equal(t,t),equal(t,f)))b:. b = true b = false