# HG changeset patch
# User nipkow
# Date 1026133384 -7200
# Node ID e4dc78f4e51e33f075e15ceaf45b5bac06d6d8c3
# Parent  ad91cf279f06477c702a6057b51f58d41ed56b72
*** empty log message ***

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