# HG changeset patch
# User nipkow
# Date 1026133318 -7200
# Node ID ad91cf279f06477c702a6057b51f58d41ed56b72
# Parent  50d82143737040926fb27965c819f405448dfa0b
*** empty log message ***

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