hol prim rec Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* m,n:. m<n+1  m = n  m<n[less_suc_imp]
cites the following:
Thm* all
Thm* (m:hnum. all
Thm* (m:hnum. (n:hnum. implies
Thm* (m:hnum. (n:hnum. (lt(m,suc(n))
Thm* (m:hnum. (n:hnum. ,implies(not(equal(m,n)),lt(m,n)))))		[hless_suc_imp]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol prim rec Sections HOLlib Doc