diff -r f3ff2549cdc8 -r 23a118849801 doc-src/TutorialI/Inductive/Star.thy
--- a/doc-src/TutorialI/Inductive/Star.thy	Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Inductive/Star.thy	Thu Aug 09 18:12:15 2001 +0200
@@ -3,6 +3,7 @@
 section{*The Reflexive Transitive Closure*}
 
 text{*\label{sec:rtc}
+\index{reflexive transitive closure!defining inductively|(}%
 An inductive definition may accept parameters, so it can express 
 functions that yield sets.
 Relations too can be defined inductively, since they are just sets of pairs.
@@ -21,7 +22,7 @@
 
 text{*\noindent
 The function @{term rtc} is annotated with concrete syntax: instead of
-@{text"rtc r"} we can read and write @{term"r*"}. The actual definition
+@{text"rtc r"} we can write @{term"r*"}. The actual definition
 consists of two rules. Reflexivity is obvious and is immediately given the
 @{text iff} attribute to increase automation. The
 second rule, @{thm[source]rtc_step}, says that we can always add one more
@@ -65,9 +66,9 @@
 apply(erule rtc.induct)
 
 txt{*\noindent
-Unfortunately, even the resulting base case is a problem
+Unfortunately, even the base case is a problem:
 @{subgoals[display,indent=0,goals_limit=1]}
-and maybe not what you had expected. We have to abandon this proof attempt.
+We have to abandon this proof attempt.
 To understand what is going on, let us look again at @{thm[source]rtc.induct}.
 In the above application of @{text erule}, the first premise of
 @{thm[source]rtc.induct} is unified with the first suitable assumption, which
@@ -150,6 +151,7 @@
 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough
 anyway, we should always pick the simplest induction schema available.
 Hence @{term rtc} is the definition of choice.
+\index{reflexive transitive closure!defining inductively|)}
 
 \begin{exercise}\label{ex:converse-rtc-step}
 Show that the converse of @{thm[source]rtc_step} also holds: