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

diff -r d694e65127ba -r 50d821437370 doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 14:55:05 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Mon Jul 08 14:59:46 2002 +0200
@@ -695,7 +695,7 @@
 proof -
   from A B show ?thesis
   proof induct
-    fix x assume "(x,z) \<in> r*"  -- "B[x := z]"
+    fix x assume "(x,z) \<in> r*"  -- "B[y := x]"
     thus "(x,z) \<in> r*" .
   next
     fix x' x y
@@ -709,7 +709,7 @@
 text{*\noindent We start the proof with \isakeyword{from}~@{text"A
 B"}. Only @{text A} is ``consumed'' by the first proof step, here
 induction. Since @{text B} is left over we don't just prove @{text
-?thesis} but in fact @{text"B \<Longrightarrow> ?thesis"}, just as in the previous
+?thesis} but @{text"B \<Longrightarrow> ?thesis"}, just as in the previous
 proof, only more elegantly. The base case is trivial. In the
 assumptions for the induction step we can see very clearly how things
 fit together and permit ourselves the obvious forward step