
diff -r d9feada9c486 -r ab4a3aef3591 doc-src/TutorialI/Misc/Itrev.thy
--- 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




