IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hnot less equal
all(
m:hnum. all(
n:hnum. equal(not(le(m,n)),lt(n,m))))
By: |
HOL "hnot_less_equal" |
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html