Added last, butlast, dropped ttl.

--- a/doc-src/Logics/HOL.tex	Thu Oct 16 10:29:56 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Oct 16 13:13:03 1997 +0200
@@ -1249,7 +1249,8 @@
   \cdx{null}    & $\alpha\,list \To bool$ & & emptiness test\\
   \cdx{hd}      & $\alpha\,list \To \alpha$ & & head \\
   \cdx{tl}      & $\alpha\,list \To \alpha\,list$ & & tail \\
-  \cdx{ttl}     & $\alpha\,list \To \alpha\,list$ & & total tail \\
+  \cdx{last}    & $\alpha\,list \To \alpha$ & & last element \\
+  \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\
   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\
   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$
         & & apply to all\\
@@ -1293,6 +1294,7 @@
 
 hd (x#xs) = x
 tl (x#xs) = xs
+tl [] = []
 
 [] @ ys = ys
 (x#xs) @ ys = x # xs @ ys