diff -r bd1d199fc58e -r 1bfdd19c1d47 doc-src/TutorialI/Inductive/Even.tex
--- a/doc-src/TutorialI/Inductive/Even.tex	Tue Nov 07 17:55:04 2000 +0100
+++ b/doc-src/TutorialI/Inductive/Even.tex	Tue Nov 07 18:38:24 2000 +0100
@@ -1,4 +1,3 @@
-% ID:         $Id$
 \section{The set of even numbers}
 
 The set of even numbers can be inductively defined as the least set
@@ -32,16 +31,12 @@
 automatically-generated names.  Here are two examples:
 %
 \begin{isabelle}
+0\ \isasymin \ even
+\rulename{even.zero}
+\par\smallskip
 n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin \
 even%
 \rulename{even.step}
-\par\medskip
-\isasymlbrakk xa\ \isasymin \ even;\isanewline
-\ P\ 0;\isanewline
-\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \
-\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline
-\ \isasymLongrightarrow \ P\ xa%
-\rulename{even.induct}
 \end{isabelle}
 
 The introduction rules can be given attributes.  Here both rules are
@@ -86,10 +81,31 @@
 
 \subsection{Rule induction}
 
-The other direction of this equivalence is proved by induction over the set
-\isa{even}.   This type of inductive argument is called \textbf{rule induction}. 
-It is the usual way of proving a property of the elements of an inductively
-defined set.
+From the definition of the set
+\isa{even}, Isabelle has
+generated an induction rule:
+\begin{isabelle}
+\isasymlbrakk xa\ \isasymin \ even;\isanewline
+\ P\ 0;\isanewline
+\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \
+\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline
+\ \isasymLongrightarrow \ P\ xa%
+\rulename{even.induct}
+\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
+rules for \isa{even}, which is the least set closed under those rules. 
+This type of inductive argument is called \textbf{rule induction}. 
+
+Apart from the double application of \isa{Suc}, the induction rule above
+resembles the familiar mathematical induction, which indeed is an instance
+of rule induction; the natural numbers can be defined inductively to be
+the least set containing \isa{0} and closed under~\isa{Suc}.
+
+Induction is the usual way of proving a property of the elements of an
+inductively defined set.  Let us prove that all members of the set
+\isa{even} are multiples of two.  
 \begin{isabelle}
 \isacommand{lemma}\ even_imp_dvd:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ dvd\ n"\isanewline
 \isacommand{apply}\ (erule\ even.induct)\isanewline
@@ -196,5 +212,8 @@
 \isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
 \isasymin \ even)"\isanewline
 \isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline
-\isacommand{done}\isanewline
+\isacommand{done}
 \end{isabelle}
+
+The even numbers example has shown how inductive definitions can be used. 
+Later examples will show that they are actually worth using.