Def pre == n:. pre(n)

is mentioned by

Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (and(lt(0,m),lt(0,n)) Thm* (m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n)))))	[hinv_pre_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (lt(0,n) Thm* (m:hnum. (n:hnum. ,equal(equal(m,pre(n)),equal(suc(m),n)))))	[hpre_suc_eq]
Thm* all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))	[hpre_sub]
Thm* all(m:hnum. equal(pre(m),sub(m,1)))	[hpre_sub1]

In prior sections: hol prim rec

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