Def 'a  'b == 'a'b

is mentioned by

Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (and Thm* (P:hnum  hbool. ((P(0) Thm* (P:hnum  hbool. (,all Thm* (P:hnum  hbool. (,(n:hnum. implies Thm* (P:hnum  hbool. (,(n:hnum. (all(m:hnum. implies(lt(m,n),P(m))) Thm* (P:hnum  hbool. (,(n:hnum. ,P(n)))) Thm* (P:hnum  hbool. ,all(n:hnum. P(n))))	[hgen_induction]
Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (exists(n:hnum. P(n)) Thm* (P:hnum  hbool. ,exists Thm* (P:hnum  hbool. ,(n:hnum. and Thm* (P:hnum  hbool. ,(n:hnum. (P(n) Thm* (P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))	[hwop]
Thm* 'a:S.  Thm* all Thm* (f:'a  hbool. all Thm* (f:'a  hbool. (x1:'a. all Thm* (f:'a  hbool. (x1:'a. (x2:'a. implies Thm* (f:'a  hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2))) Thm* (f:'a  hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2))))))	[hfun_eq_lemma]

In prior sections: hol bool hol num hol prim rec

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