--- a/src/Doc/Prog_Prove/Logic.thy Tue Jun 16 11:31:22 2015 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Mon Jun 29 13:49:21 2015 +0200
@@ -813,7 +813,7 @@
text{*
The single @{text r} step is performed after rather than before the @{text star'}
steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"} and
-@{prop "star r x y \<Longrightarrow> star r' x y"}. You may need lemmas.
+@{prop "star r x y \<Longrightarrow> star' r x y"}. You may need lemmas.
Note that rule induction fails
if the assumption about the inductive predicate is not the first assumption.
\endexercise