Def pre(n) == if n=0 then 0 else n-1 fi 

is mentioned by

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* n:. n>0  pre(n) = n-1	[pre_nuprl]
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]

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