Def simp_rec == x:'a. f:'a'a. n:. ncompose(f;n;x)

is mentioned by

Thm* 'a:S, x:'a, f:('a'a). Thm* simp_rec(x,f,0) = x & (m:. simp_rec(x,f,m+1) = f(simp_rec(x,f,m)))	[simp_rec_thm]
Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. and Thm* (x:'a. (f:'a  'a. (equal(simp_rec(x,f,0),x) Thm* (x:'a. (f:'a  'a. ,all Thm* (x:'a. (f:'a  'a. ,(m:hnum. equal Thm* (x:'a. (f:'a  'a. ,(m:hnum. (simp_rec(x,f,suc(m)) Thm* (x:'a. (f:'a  'a. ,(m:hnum. ,f(simp_rec(x,f,m)))))))	[hsimp_rec_thm]
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* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. equal Thm* (x:'a. (f:'a  'a. (n:hnum. (simp_rec(x,f,n) Thm* (x:'a. (f:'a  'a. (n:hnum. ,simp_rec_fun(x,f,suc(n),n)))))	[hsimp_rec_wd]
Def prim_rec_fun Def == x:'a. f:'a'a. simp_rec Def == x:'a. f:'a'a. ((n:. x) Def == x:'a. f:'a'a. ,fun:'a. n:. f(fun(pre(n)),n))	[hprim_rec_fun]

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