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

is mentioned by

Thm* all(n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))	[hless_or_eq_add]
Thm* all(m:hnum. all(n:hnum. or(lt(m,n),le(n,m))))	[hless_cases]
Thm* all(m:hnum. or(equal(0,m),lt(0,m)))	[hless_0_cases]
Thm* all(m:hnum. or(equal(m,0),exists(n:hnum. equal(m,suc(n)))))	[hnum_cases]
Thm* all(m:hnum. all(n:hnum. equal(ge(m,n),or(gt(m,n),equal(m,n)))))	[hgreater_or_eq]
Thm* all(m:hnum. all(n:hnum. equal(le(m,n),or(lt(m,n),equal(m,n)))))	[hless_or_eq]

In prior sections: hol bool hol prim rec

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