--- a/doc-src/Logics/HOL.tex Tue Dec 30 11:14:09 1997 +0100
+++ b/doc-src/Logics/HOL.tex Tue Dec 30 13:43:39 1997 +0100
@@ -1281,6 +1281,7 @@
\index{#@{\tt[]} symbol}
\index{#@{\tt\#} symbol}
\index{"@@{\tt\at} symbol}
+\index{*"! symbol}
\begin{constants}
\it symbol & \it meta-type & \it priority & \it description \\
\tt[] & $\alpha\,list$ & & empty list\\
@@ -1297,13 +1298,13 @@
\cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$
& & filter functional\\
\cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\
- \sdx{mem} & $[\alpha,\alpha\,list]\To bool$ & Left 55 & membership\\
+ \sdx{mem} & $\alpha \To \alpha\,list \To bool$ & Left 55 & membership\\
\cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
& iteration \\
\cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\
\cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\
\cdx{length} & $\alpha\,list \To nat$ & & length \\
- \cdx{nth} & $nat \To \alpha\,list \To \alpha$ & & indexing \\
+ \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\
\cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&
take or drop a prefix \\
\cdx{takeWhile},\\
@@ -1363,8 +1364,8 @@
length([]) = 0
length(x#xs) = Suc(length(xs))
-nth 0 xs = hd xs
-nth (Suc n) xs = nth n (tl xs)
+xs!0 = hd xs
+xs!(Suc n) = (tl xs)!n
take n [] = []
take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
--- a/doc-src/Logics/logics.ind Tue Dec 30 11:14:09 1997 +0100
+++ b/doc-src/Logics/logics.ind Tue Dec 30 13:43:39 1997 +0100
@@ -1,6 +1,6 @@
\begin{theindex}
- \item {\tt !} symbol, 60, 62, 69, 70
+ \item {\tt !} symbol, 60, 62, 69, 70, 82
\item {\tt[]} symbol, 82
\item {\tt\#} symbol, 82
\item {\tt\#*} symbol, 47, 128
@@ -600,7 +600,6 @@
\item {\tt notL} theorem, 107
\item {\tt notnotD} theorem, 11, 66
\item {\tt notR} theorem, 107
- \item {\tt nth} constant, 82
\item {\tt null} constant, 82
\indexspace