doc-src/TutorialI/Types/numerics.tex

--- a/doc-src/TutorialI/Types/numerics.tex	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
 \section{Numbers}
 \label{sec:numbers}
 
+\index{numbers|(}%
 Until now, our numerical examples have used the type of \textbf{natural
 numbers},
 \isa{nat}.  This is a recursive datatype generated by the constructors
@@ -45,7 +46,7 @@
 They begin 
 with a number sign (\isa{\#}), have an optional minus sign (\isa{-}) and 
 then one or more decimal digits. Examples are \isa{\#0}, \isa{\#-3} 
-and \isa{\#441223334678}.
+and \isa{\#441223334678}.\REMARK{will need updating?}
 
 Literals look like constants, but they abbreviate 
 terms, representing the number in a two's complement binary notation. 
@@ -110,7 +111,7 @@
 in a variety of additive types. The symbols \sdx{1} and \sdx{2} are 
 not constants but abbreviations for \isa{Suc 0} and \isa{Suc(Suc 0)},
 respectively. The literals \isa{\#0}, \isa{\#1} and \isa{\#2}  are
-syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will
+syntactically different from \isa{0}, \isa{1} and \isa{2}. You  will\REMARK{will need updating?}
 sometimes prefer one notation to the other. Literals are  obviously
 necessary to express large values, while \isa{0} and \isa{Suc}  are needed
 in order to match many theorems, including the rewrite  rules for primitive
@@ -224,7 +225,7 @@
 d))
 \rulename{nat_diff_split}
 \end{isabelle}
-For example, it proves the following fact, which lies outside the scope of
+For example, this splitting proves the following fact, which lies outside the scope of
 linear arithmetic:\REMARK{replace by new example!}
 \begin{isabelle}
 \isacommand{lemma}\ "(n-1)*(n+1)\ =\ n*n\ -\ 1"\isanewline
@@ -245,8 +246,10 @@
 +\ z)
 \rulename{add_left_commute}
 \end{isabelle}
-The name \isa{add_ac} refers to the list of all three theorems, similarly
-there is \isa{mult_ac}.  Here is an example of the sorting effect.  Start
+The name \isa{add_ac}\index{*add_ac (theorems)} 
+refers to the list of all three theorems; similarly
+there is \isa{mult_ac}.\index{*mult_ac (theorems)} 
+Here is an example of the sorting effect.  Start
 with this goal:
 \begin{isabelle}
 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\
@@ -297,9 +300,11 @@
 
 Concerning simplifier tricks, we have no need to eliminate subtraction: it
 is well-behaved.  As with the natural numbers, the simplifier can sort the
-operands of sums and products.  The name \isa{zadd_ac} refers to the
+operands of sums and products.  The name \isa{zadd_ac}\index{*zadd_ac (theorems)}
+refers to the
 associativity and commutativity theorems for integer addition, while
-\isa{zmult_ac} has the analogous theorems for multiplication.  The
+\isa{zmult_ac}\index{*zmult_ac (theorems)}
+has the analogous theorems for multiplication.  The
 prefix~\isa{z} in many theorem names recalls the use of $\mathbb{Z}$ to
 denote the set of integers.
 
@@ -450,4 +455,5 @@
 about limits, differentiation and integration~\cite{fleuriot-jcm}.  The
 development defines an infinitely large number, \isa{omega} and an
 infinitely small positive number, \isa{epsilon}.  The 
-relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.
+relation $x\approx y$ means ``$x$ is infinitely close to~$y$''.%
+\index{numbers|)}
\ No newline at end of file