PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
num
cases
m
:
.
m
= 0
(
n
:
.
m
=
n
+1
)
By:
RewriteOfThm Thm* all(
m
:hnum. or(equal(
m
,0),exists(
n
:hnum. equal(
m
,suc(
n
)))))
(SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
arithmetic
3
Sections
HOLlib
Doc