Def suc == n:. n+1

is mentioned by

Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (and(P(0),all(n:hnum. implies(P(n),P(suc(n))))) Thm* (P:hnum  hbool. ,all(n:hnum. P(n))))	[hinduction]
Thm* all(m:hnum. all(n:hnum. implies(equal(suc(m),suc(n)),equal(m,n))))	[hinv_suc]
Thm* all(n:hnum. not(equal(suc(n),0)))	[hnot_suc]
Thm* all(m:hnum. equal(suc(m),abs_num(suc_rep(rep_num(m)))))	[hsuc_def]

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