Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* 'a:S, e:'a, f:('a'a). Thm* (fn1:('a). fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n))) Thm* & (fn1,y:('a). Thm* & (fn1(0) = e & (n:. fn1(n+1) = f(fn1(n),n)) Thm* & (& y(0) = e Thm* & (& (n:. y(n+1) = f(y(n),n)) Thm* & ( Thm* & (fn1 = y)	[num_axiom]
Thm* 'a:S, x:'a, f:('a'a), n:. fun:('a). simp_rec_rel(fun,x,f,n)	[simp_rec_exists]
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]

In prior sections: core fun 1 hol hol bool

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