Def not == p:. p

is mentioned by

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* all(n:hnum. all(m:hnum. not(equal(suc(add(n,n)),add(m,m)))))	[hnot_odd_eq_even]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),not(lt(n,suc(m))))))	[hless_suc_not]
Thm* all(m:hnum. all(n:hnum. equal(not(lt(m,n)),le(n,m))))	[hnot_less]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),le(n,m)))))	[hless_eq_antisym]
Thm* all(m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n)))))	[hless_add_nonzero]
Thm* all Thm* (m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m))))	[hless_cases_imp]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (and(lt(m,n),not(equal(n,suc(m)))) Thm* (m:hnum. (n:hnum. ,lt(suc(m),n))))	[hless_not_suc]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (and(lt(m,n),not(equal(suc(m),n))) Thm* (m:hnum. (n:hnum. ,lt(suc(m),n))))	[hless_suc_eq_cor]
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]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,suc(m))))))	[hless_less_suc]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,m)))))	[hless_antisym]
Thm* all(n:hnum. not(equal(0,suc(n))))	[hsuc_not]
Thm* and(equal(odd(0),f),all(n:hnum. equal(odd(suc(n)),not(odd(n)))))	[hodd_wd]
Thm* and(equal(even(0),t),all(n:hnum. equal(even(suc(n)),not(even(n)))))	[heven_wd]

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