Def fact(n) == if n=0 then 1 else nfact(n-1) fi   (recursive)

is mentioned by

Thm* n:. n>0  fact(n) = nfact(n-1)	[fact_pos]
Thm* fact(0) = 1	[fact_zero]
Def fact == n:. fact(n)	[hfact]

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