diff -r ad91cf279f06 -r e4dc78f4e51e doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 15:01:58 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 15:03:04 2002 +0200
@@ -699,10 +699,10 @@
     thus "(x,z) \<in> r*" .
   next
     fix x' x y
-    assume step: "(x',x) \<in> r" and
+    assume 1: "(x',x) \<in> r" and
            IH: "(y,z) \<in> r* \<Longrightarrow> (x,z) \<in> r*" and
            B:  "(y,z) \<in> r*"
-    from step IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
+    from 1 IH[OF B] show "(x',z) \<in> r*" by(rule rtc.step)
   qed
 qed