Def simp_rec_fun
Def == x:'a. f:'a'a. n:. @fun:'a. (simp_rec_rel(fun,x,f,n))

is mentioned by

Thm* 'a:S, n:, f:('a'a), x:'a. Thm* (fun:('a). simp_rec_rel(fun,x,f,n)) Thm*  Thm* simp_rec_fun(x,f,n,0) = x Thm* & (m:. m<n  simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))	[simp_rec_fun_lemma]
Thm* 'a:S.  Thm* all Thm* (n:hnum. all Thm* (n:hnum. (f:'a Thm* (n:hnum. ( 'a. all Thm* (n:hnum. ( 'a. (x:'a. equal Thm* (n:hnum. ( 'a. (x:'a. (exists(fun:hnum  'a. simp_rec_rel(fun,x,f,n)) Thm* (n:hnum. ( 'a. (x:'a. ,and Thm* (n:hnum. ( 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x) Thm* (n:hnum. ( 'a. (x:'a. ,,all Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. implies Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. (lt(m,n) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,equal Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m)) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))	[hsimp_rec_fun_lemma]
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]
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_fun(x,f,n) Thm* (x:'a. (f:'a  'a. (n:hnum. ,select Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. simp_rec_rel Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. (fun Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,x Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,f Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,n))))))	[hsimp_rec_fun_wd]

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