doc-src/Logics/HOL.tex
 changeset 3881 73be08b4da3f parent 3489 afa802078173 child 3959 033633d9a032
--- 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