hol
arithmetic
3
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
:
.
0 =
n
+1
[suc_not]
cites the following:
Thm* all(
n
:hnum. not(equal(0,suc(
n
))))
[hsuc_not]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
3
Sections
HOLlib
Doc
n:
. 
0 = n+1 
n:hnum. not(equal(0,suc(n))))n:. 0 = n+1 n:hnum. not(equal(0,suc(n))))