--- a/doc-src/TutorialI/Misc/Itrev.thy Thu Apr 04 19:43:25 2002 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Mon Apr 08 14:39:16 2002 +0200
@@ -115,7 +115,7 @@
This prevents trivial failures like the one above and does not affect the
validity of the goal. However, this heuristic should not be applied blindly.
It is not always required, and the additional quantifiers can complicate
-matters in some cases, The variables that should be quantified are typically
+matters in some cases. The variables that should be quantified are typically
those that change in recursive calls.
A final point worth mentioning is the orientation of the equation we just