diff -r dd4253d5dd82 -r 9627a75eb32a src/Doc/Prog_Prove/Logic.thy
--- 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