diff -r 50d821437370 -r ad91cf279f06 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 14:59:46 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 15:01:58 2002 +0200
@@ -695,7 +695,7 @@
 proof -
   from A B show ?thesis
   proof induct
-    fix x assume "(x,z) \<in> r*"  -- "B[y := x]"
+    fix x assume "(x,z) \<in> r*"  -- {*@{text B}[@{text y} := @{text x}]*}
     thus "(x,z) \<in> r*" .
   next
     fix x' x y