Def not == p:. p

is mentioned by

Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),not(equal(m,n)))))	[hless_not_eq]
Thm* all(m:hnum. all(n:hnum. implies(equal(m,n),not(lt(m,n)))))	[hnot_less_eq]
Thm* all(n:hnum. not(equal(suc(n),n)))	[hsuc_id]
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]
Thm* all(n:hnum. not(lt(n,0)))	[hnot_less_0]
Thm* all(n:hnum. not(lt(n,n)))	[hless_refl]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. equal Thm* (m:hnum. (n:hnum. (lt(m,n) Thm* (m:hnum. (n:hnum. ,exists Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. and Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. (all Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ((n:hnum. implies(P(suc(n)),P(n))) Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ,and(P(m),not(P(n))))))))	[hless_def]

In prior sections: hol bool hol num

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