Def null == l:'a List. null(l)

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. and(null(nil),all(h:'a. all(t:hlist('a). not(null(cons(h,t))))))	[hnull_char]
Thm* 'a:S.  Thm* and Thm* (equal(null(nil),t) Thm* ,all(t:hlist('a). all(h:'a. equal(null(cons(h,t)),f))))	[hnull_def]

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