--- 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