Def not == p:. p

is mentioned by

Thm* 'a:S. all(l:hlist('a). implies(not(null(l)),equal(cons(hd(l),tl(l)),l)))	[hcons_char]
Thm* 'a:S.  Thm* all Thm* (h1:'a. all Thm* (h1:'a. (h2:'a. implies Thm* (h1:'a. (h2:'a. (not(equal(h1,h2)) Thm* (h1:'a. (h2:'a. ,all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). all Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). not Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (equal Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). ((cons(h1,l1) Thm* (h1:'a. (h2:'a. ,(l1:hlist('a). (l2:hlist('a). (,cons(h2,l2))))))))	[hnot_eq_list]
Thm* 'a:S.  Thm* all Thm* (l1:hlist('a). all Thm* (l1:hlist('a). (l2:hlist('a). implies Thm* (l1:hlist('a). (l2:hlist('a). (not(equal(l1,l2)) Thm* (l1:hlist('a). (l2:hlist('a). ,all Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. all Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. not Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (equal Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. ((cons(h1,l1) Thm* (l1:hlist('a). (l2:hlist('a). ,(h1:'a. (h2:'a. (,cons(h2,l2))))))))	[hlist_not_eq]
Thm* 'a:S. all(t:hlist('a). all(h:'a. not(equal(cons(h,t),nil))))	[hnot_cons_nil]
Thm* 'a:S. all(t:hlist('a). all(h:'a. not(equal(nil,cons(h,t)))))	[hnot_nil_cons]
Thm* 'a:S. and(null(nil),all(h:'a. all(t:hlist('a). not(null(cons(h,t))))))	[hnull_char]

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