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))

is mentioned

In prior sections: hol prim rec

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html