Def implies == p:. q:. pq

is mentioned by

Thm* 'a:S.  Thm* all Thm* (n:hnum. all Thm* (n:hnum. (f:'a Thm* (n:hnum. ( 'a. all Thm* (n:hnum. ( 'a. (x:'a. equal Thm* (n:hnum. ( 'a. (x:'a. (exists(fun:hnum  'a. simp_rec_rel(fun,x,f,n)) Thm* (n:hnum. ( 'a. (x:'a. ,and Thm* (n:hnum. ( 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x) Thm* (n:hnum. ( 'a. (x:'a. ,,all Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. implies Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. (lt(m,n) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,equal Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m)) Thm* (n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))	[hsimp_rec_fun_lemma]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),not(equal(m,n)))))	[hless_not_eq]
Thm* all(m:hnum. all(n:hnum. implies(equal(m,n),not(lt(m,n)))))	[hnot_less_eq]
Thm* all(m:hnum. all(n:hnum. implies(equal(suc(m),n),lt(m,n))))	[heq_less]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (lt(m,suc(n)) Thm* (m:hnum. (n:hnum. ,implies(not(equal(m,n)),lt(m,n)))))	[hless_suc_imp]
Thm* all(m:hnum. all(n:hnum. implies(or(equal(m,n),lt(m,n)),lt(m,suc(n)))))	[hless_lemma2]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,suc(n)),or(equal(m,n),lt(m,n)))))	[hless_lemma1]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),lt(m,suc(n)))))	[hless_suc]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),lt(suc(m),suc(n)))))	[hless_mono]
Thm* all(m:hnum. all(n:hnum. implies(lt(suc(m),n),lt(m,n))))	[hsuc_less]
Thm* 'a:S.  Thm* all Thm* (fun:hnum Thm* ( 'a. all Thm* ( 'a. (x:'a. all Thm* ( 'a. (x:'a. (f:'a  'a. all Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. equal Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. (simp_rec_rel(fun,x,f,n) Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,and Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,(equal(fun(0),x) Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,all Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. implies Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. (lt(m,n) Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,equal Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,(fun(suc(m)) Thm* ( 'a. (x:'a. (f:'a  'a. (n:hnum. ,,(m:hnum. ,,f(fun(m)))))))))))	[hsimp_rec_rel_wd]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. equal Thm* (m:hnum. (n:hnum. (lt(m,n) Thm* (m:hnum. (n:hnum. ,exists Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. and Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. (all Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ((n:hnum. implies(P(suc(n)),P(n))) Thm* (m:hnum. (n:hnum. ,(P:hnum  hbool. ,and(P(m),not(P(n))))))))	[hless_def]

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