Def prim_rec == x:'a. f:'a'a. m:. prim_rec_fun(x,f,m,pre(m))

is mentioned by

Thm* 'a:S, x:'a, f:('a'a). Thm* prim_rec(x,f,0) = x & (m:. prim_rec(x,f,m+1) = f(prim_rec(x,f,m),m))	[prim_rec_thm]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  hnum  'a. and Thm* (x:'a. (f:'a  hnum  'a. (equal(prim_rec(x,f,0),x) 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,suc(m)) Thm* (x:'a. (f:'a  hnum  'a. ,(m:hnum. ,f(prim_rec(x,f,m),m))))))	[hprim_rec_thm]
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]

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