Def or == p:. q:. p  q

is mentioned by

Thm* all(m:hnum. all(n:hnum. equal(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))	[hless_thm]
Thm* all(m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n)))))	[hless_lemma2]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))	[hless_lemma1]

In prior sections: hol bool

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html