# HG changeset patch
# User nipkow
# Date 877000383 -7200
# Node ID 73be08b4da3fd927a05471a2c9c4b20ca3184bc0
# Parent  d93c62ec97a6694fc9cde0278a14eee3c84f8ebe
Added last, butlast, dropped ttl.

diff -r d93c62ec97a6 -r 73be08b4da3f doc-src/Logics/HOL.tex
--- 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