Def select == p:'a. @x:'a. (p(x))

is mentioned by

Thm* all Thm* (m:hnum. equal Thm* (m:hnum. (pre(m) Thm* (m:hnum. ,cond(equal(m,0),0,select(n:hnum. equal(m,suc(n))))))

[hpre_def]

Thm* 'a:S.  Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a  'a. all Thm* (x:'a. (f:'a  'a. (n:hnum. equal Thm* (x:'a. (f:'a  'a. (n:hnum. (simp_rec_fun(x,f,n) Thm* (x:'a. (f:'a  'a. (n:hnum. ,select Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. simp_rec_rel Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. (fun Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,x Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,f Thm* (x:'a. (f:'a  'a. (n:hnum. ,(fun:hnum  'a. ,n))))))

[hsimp_rec_fun_wd]

In prior sections: hol bool hol num

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