Def list_accum(x,a.f(x;a);y;l)
Def == Case of l; nil  y ; b.l'  list_accum(x,a.f(x;a);f(y;b);l')
Def (recursive)

is not otherwise mentioned in this or prior sections.

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