Def  == {i:| 0i }

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). 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, x:'a, f:('a'a). Thm* (n:. prim_rec_fun(x,f,0,n) = x) Thm* & (m,n:. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))	[prim_rec_eqn]
Thm* pre(0) = 0 & (m:. pre(m+1) = m)	[pre_suc]
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* m:. m<m+1 & m<m+1+1	[less_suc_suc]
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]
Thm* m,n:. m<n  m = n	[less_not_eq]
Thm* m,n:. m = n  m<n	[not_less_eq]
Thm* n:. n+1 = n	[suc_id]
Thm* m,n:. m+1 = n    m<n	[eq_less]
Thm* n:. 0<n+1	[less_0]
Thm* m,n:. m<n+1  m = n  m<n	[less_suc_imp]
Thm* m,n:. m<n+1  m = n  m<n	[less_thm]
Thm* m,n:. m = n  m<n  m<n+1	[less_lemma2]
Thm* m,n:. m<n+1  m = n  m<n	[less_lemma1]
Thm* m,n:. m<n  m<n+1	[less_suc]
Thm* n:. n<n+1	[less_suc_refl]
Thm* m,n:. m<n  m+1<n+1	[less_mono]
Thm* n:. n<0	[not_less_0]
Thm* m,n:. m+1<n  m<n	[suc_less]
Thm* n:. n<n	[less_refl]
Thm* m,n:. m+1 = n+1    m = n	[inv_suc_eq]
Thm* n:. n>0  pre(n) = n-1	[pre_nuprl]
Thm* n:. pre(n)	[pre_wf]
Def prim_rec == x:'a. f:'a'a. m:. prim_rec_fun(x,f,m,pre(m))	[hprim_rec]
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]
Def pre == n:. pre(n)	[hpre]
Def simp_rec == x:'a. f:'a'a. n:. ncompose(f;n;x)	[hsimp_rec]
Def simp_rec_fun Def == x:'a. f:'a'a. n:. @fun:'a. (simp_rec_rel(fun,x,f,n))	[hsimp_rec_fun]
Def simp_rec_rel Def == fun:'a. x:'a. f:'a'a. n:. (fun(0) = x Def == & (m:. m<n  fun(m+1) = f(fun(m))))	[hsimp_rec_rel]
Def lt == m:. n:. m<n	[hlt]

In prior sections: int 1 bool 1 hol num hol min

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