# HG changeset patch
# User nipkow
# Date 1383150059 -3600
# Node ID 2fa338fd0a280d82bbcf68d51ef682e96f716b2a
# Parent  c0c453ce70a759b3d0b833962840a468a19b1926
tuned text

diff -r c0c453ce70a7 -r 2fa338fd0a28 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Tue Oct 29 13:48:18 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy	Wed Oct 30 17:20:59 2013 +0100
@@ -799,12 +799,10 @@
 
 text{*
 The single @{text r} step is performer after rather than before the @{text star'}
-steps. Prove @{prop "star' r x y \<Longrightarrow> star r x y"}. You may need a lemma.
-The other direction can also be proved but
-you have to be careful how to formulate the lemma it will require:
-make sure that the assumption about the inductive predicate
-is the first assumption. Assumptions preceding the inductive predicate do not
-take part in the induction.
+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.
+Note that rule induction fails
+if the assumption about the inductive predicate is not the first assumption.
 \endexercise
 
 \ifsem