Def hd == l:'a List. if null(l) then arb('a) else head(l) fi 

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(hd(cons(h,t)),h)))	[hhd_wd]

In prior sections: hol list 1

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