PrintForm
Definitions
hol
arithmetic
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hpre
sub
all(
m
:hnum. all(
n
:hnum. equal(pre(sub(
m
,
n
)),sub(pre(
m
),
n
))))
By:
HOL "hpre_sub"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
hol
arithmetic
2
Sections
HOLlib
Doc
all(
m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n)))) all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))
