diff -r 48c63b87566e -r 6f6892bea902 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Thu Feb 15 00:53:45 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Thu Feb 15 11:15:39 2001 +0100
@@ -2,7 +2,7 @@
 \section{The Set of Even Numbers}
 
 The set of even numbers can be inductively defined as the least set
-containing 0 and closed under the operation ${\cdots}+2$.  Obviously,
+containing 0 and closed under the operation $+2$.  Obviously,
 \emph{even} can also be expressed using the divides relation (\isa{dvd}). 
 We shall prove below that the two formulations coincide.  On the way we
 shall examine the primary means of reasoning about inductively defined
@@ -73,7 +73,7 @@
 Our ultimate goal is to prove the equivalence between the traditional
 definition of \isa{even} (using the divides relation) and our inductive
 definition.  One direction of this equivalence is immediate by the lemma
-just proved, whose \isa{intro!} attribute ensures it will be used.
+just proved, whose \isa{intro!} attribute ensures it is applied automatically.
 \begin{isabelle}
 \isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
 \isacommand{by}\ (auto\ simp\ add:\ dvd_def)
@@ -95,7 +95,7 @@
 \end{isabelle}
 A property \isa{P} holds for every even number provided it
 holds for~\isa{0} and is closed under the operation
-\isa{Suc(Suc\(\cdots\))}.  Then \isa{P} is closed under the introduction
+\isa{Suc(Suc \(\cdot\))}.  Then \isa{P} is closed under the introduction
 rules for \isa{even}, which is the least set closed under those rules. 
 This type of inductive argument is called \textbf{rule induction}.