diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -64,7 +64,7 @@
 @{subgoals[display,indent=0,margin=65]}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
-@{term"[]"}. The corresponding heuristic:
+argument, @{term"[]"}.  This suggests a heuristic:
 \begin{quote}
 \emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
@@ -109,11 +109,13 @@
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
 applied blindly.
+The variables that require generalization are typically those that 
+change in recursive calls.
 
 In general, if you have tried the above heuristics and still find your
 induction does not go through, and no obvious lemma suggests itself, you may
 need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. In a nutshell: you
+the problem at hand and is beyond simple rules of thumb.  You
 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
 to learn about some advanced techniques for inductive proofs.