Def exp(m;n) == if n=0 then 1 else mexp(m;n-1) fi   (recursive)

is mentioned by

Thm* m,n:. n>0  exp(m;n) = mexp(m;n-1)	[exp_pos]
Thm* m:. exp(m;0) = 1	[exp_zero]
Def exp == m:. n:. exp(m;n)	[hexp]

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