IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def odd(n) == if n=
0 then false
else 
odd(n-1) fi (recursive)
is mentioned by
Thm* n: . n>0  odd(n) =  odd(n-1) | [odd_pos] |
Thm* odd(0) = false | [odd_zero] |
Def odd == n: . odd(n) | [hodd] |
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html