# HG changeset patch
# User nipkow
# Date 883485819 -3600
# Node ID 5ed72705c201cc9cd88116b51126eb78e52545a6
# Parent  337c073de95e772b2c73d618d7c2f9c9442f791d
nth -> !

diff -r 337c073de95e -r 5ed72705c201 doc-src/Logics/HOL.tex
--- 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)
diff -r 337c073de95e -r 5ed72705c201 doc-src/Logics/logics.ind
--- 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