Def tl == l:'a List. tl(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.  Thm* and Thm* (all(l:hlist('a). equal(el(0,l),hd(l))) Thm* ,all(l:hlist('a). all(n:hnum. equal(el(suc(n),l),el(n,tl(l))))))	[hel_wd]
Thm* 'a:S. all(t:hlist('a). all(h:'a. equal(tl(cons(h,t)),t)))	[htl_wd]

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