tuned text
authornipkow
Wed, 30 Oct 2013 17:20:59 +0100
changeset 54217 2fa338fd0a28
parent 54216 c0c453ce70a7
child 54218 07c0c121a8dc
tuned text
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