Def pre == n:. pre(n)

is mentioned by

Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  hnum  'a. and Thm* (x:'a. (f:'a  hnum  'a. (all(n:hnum. equal(prim_rec_fun(x,f,0,n),x)) Thm* (x:'a. (f:'a  hnum  'a. ,all Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. all Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. equal Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. (prim_rec_fun Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ((x Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. (,f Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. (,suc(m) Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. (,n) Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,f Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,(prim_rec_fun Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,((x Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,(,f Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,(,m Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,(,pre(n)) Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. (n:hnum. ,,n)))))))	[hprim_rec_eqn]
Thm* and(equal(pre(0),0),all(m:hnum. equal(pre(suc(m)),m)))	[hpre_suc]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  hnum  'a. all Thm* (x:'a. (f:'a  hnum  'a. (m:hnum. equal Thm* (x:'a. (f:'a  hnum  'a. (m:hnum. (prim_rec(x,f,m) Thm* (x:'a. (f:'a  hnum  'a. (m:hnum. ,prim_rec_fun(x,f,m,pre(m))))))	[hprim_rec_wd]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  hnum  'a. equal Thm* (x:'a. (f:'a  hnum  'a. (prim_rec_fun(x,f) Thm* (x:'a. (f:'a  hnum  'a. ,simp_rec Thm* (x:'a. (f:'a  hnum  'a. ,((n:hnum. x) Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. f Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. (fun(pre(n)) Thm* (x:'a. (f:'a  hnum  'a. ,,fun:hnum  'a. n:hnum. ,n)))))	[hprim_rec_fun_wd]
Thm* all Thm* (m:hnum. equal Thm* (m:hnum. (pre(m) Thm* (m:hnum. ,cond(equal(m,0),0,select(n:hnum. equal(m,suc(n))))))	[hpre_def]

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