diff -r b3b61ea9632c -r c315dda16748 doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Thu Jul 12 16:33:36 2001 +0200
@@ -1,6 +1,7 @@
 % $Id$
 \section{The Set of Even Numbers}
 
+\index{even numbers!defining inductively|(}%
 The set of even numbers can be inductively defined as the least set
 containing 0 and closed under the operation $+2$.  Obviously,
 \emph{even} can also be expressed using the divides relation (\isa{dvd}). 
@@ -11,7 +12,7 @@
 \subsection{Making an Inductive Definition}
 
 Using \isacommand{consts}, we declare the constant \isa{even} to be a set
-of natural numbers. The \isacommand{inductive} declaration gives it the
+of natural numbers. The \commdx{inductive} declaration gives it the
 desired properties.
 \begin{isabelle}
 \isacommand{consts}\ even\ ::\ "nat\ set"\isanewline
@@ -41,8 +42,10 @@
 \rulename{even.step}
 \end{isabelle}
 
-The introduction rules can be given attributes.  Here both rules are
-specified as \isa{intro!}, directing the classical reasoner to 
+The introduction rules can be given attributes.  Here
+both rules are specified as \isa{intro!},%
+\index{intro"!@\isa {intro"!} (attribute)}
+directing the classical reasoner to 
 apply them aggressively. Obviously, regarding 0 as even is safe.  The
 \isa{step} rule is also safe because $n+2$ is even if and only if $n$ is
 even.  We prove this equivalence later.
@@ -83,6 +86,7 @@
 \subsection{Rule Induction}
 \label{sec:rule-induction}
 
+\index{rule induction|(}%
 From the definition of the set
 \isa{even}, Isabelle has
 generated an induction rule:
@@ -161,6 +165,7 @@
 \subsection{Generalization and Rule Induction}
 \label{sec:gen-rule-induction}
 
+\index{generalizing for induction}%
 Before applying induction, we typically must generalize
 the induction formula.  With rule induction, the required generalization
 can be hard to find and sometimes requires a complete reformulation of the
@@ -200,7 +205,8 @@
 \end{isabelle}
 The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is
 even.  The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to
-\isa{n}, matching the assumption.
+\isa{n}, matching the assumption.%
+\index{rule induction|)}  %the sequel isn't really about induction
 
 \medskip
 Using our lemma, we can easily prove the result we originally wanted:
@@ -210,8 +216,8 @@
 \end{isabelle}
 
 We have just proved the converse of the introduction rule \isa{even.step}. 
-This suggests proving the following equivalence.  We give it the \isa{iff}
-attribute because of its obvious value for simplification.
+This suggests proving the following equivalence.  We give it the
+\attrdx{iff} attribute because of its obvious value for simplification.
 \begin{isabelle}
 \isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
 \isasymin \ even)"\isanewline
@@ -221,10 +227,12 @@
 
 \subsection{Rule Inversion}\label{sec:rule-inversion}
 
-Case analysis on an inductive definition is called \textbf{rule inversion}. 
-It is frequently used in proofs about operational semantics.  It can be
-highly effective when it is applied automatically.  Let us look at how rule
-inversion is done in Isabelle/HOL\@.
+\index{rule inversion|(}%
+Case analysis on an inductive definition is called \textbf{rule
+inversion}.  It is frequently used in proofs about operational
+semantics.  It can be highly effective when it is applied
+automatically.  Let us look at how rule inversion is done in
+Isabelle/HOL\@.
 
 Recall that \isa{even} is the minimal set closed under these two rules:
 \begin{isabelle}
@@ -258,7 +266,8 @@
 \isacommand{inductive\_cases}\ Suc_Suc_cases\ [elim!]:
 \ "Suc(Suc\ n)\ \isasymin \ even"
 \end{isabelle}
-The \isacommand{inductive\_cases} command generates an instance of the
+The \commdx{inductive\protect\_cases} command generates an instance of
+the
 \isa{cases} rule for the supplied pattern and gives it the supplied name:
 %
 \begin{isabelle}
@@ -273,8 +282,10 @@
 (list ``cons''); freeness reasoning discards all but one or two cases.
 
 In the \isacommand{inductive\_cases} command we supplied an
-attribute, \isa{elim!}, indicating that this elimination rule can be applied
-aggressively.  The original
+attribute, \isa{elim!},
+\index{elim"!@\isa {elim"!} (attribute)}%
+indicating that this elimination rule can be
+applied aggressively.  The original
 \isa{cases} rule would loop if used in that manner because the
 pattern~\isa{a} matches everything.
 
@@ -300,10 +311,12 @@
 as an elimination rule.
 
 To summarize, every inductive definition produces a \isa{cases} rule.  The
-\isacommand{inductive\_cases} command stores an instance of the \isa{cases}
-rule for a given pattern.  Within a proof, the \isa{ind_cases} method
-applies an instance of the \isa{cases}
+\commdx{inductive\protect\_cases} command stores an instance of the
+\isa{cases} rule for a given pattern.  Within a proof, the
+\isa{ind_cases} method applies an instance of the \isa{cases}
 rule.
 
 The even numbers example has shown how inductive definitions can be
-used.  Later examples will show that they are actually worth using.
+used.  Later examples will show that they are actually worth using.%
+\index{rule inversion|)}%
+\index{even numbers!defining inductively|)}