PrintForm
Definitions
Lemmas
hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mult
right
1
m
:
.
m
1 =
m
By:
RewriteOfThm
Thm*
all(
m
:hnum. equal(mult(
m
,1),
m
))
(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
4
Sections
HOLlib
Doc