Def cond == b:. p:'a. q:'a. if b then p else q fi 

is mentioned by

Thm* and Thm* (all(m:hnum. equal(sub(0,m),0)) Thm* ,all Thm* ,(m:hnum. all Thm* ,(m:hnum. (n:hnum. equal(sub(suc(m),n),cond(lt(m,n),0,suc(sub(m,n)))))))

[hsub_wd]

In prior sections: hol bool hol prim rec

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