# HG changeset patch
# User nipkow
# Date 1440491310 -7200
# Node ID 5f985515728e652c466a4449f677edf4fdec50d3
# Parent  0be2726382d9a34c23ea7d63b06746e663da87cd
tuned exercise

diff -r 0be2726382d9 -r 5f985515728e src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Aug 24 21:24:17 2015 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Tue Aug 25 10:28:30 2015 +0200
@@ -1124,8 +1124,8 @@
 \mbox{@{text "alpha list"}} is a balanced
 string of parentheses. More precisely, define a recursive function
 @{text "balanced :: nat \<Rightarrow> alpha list \<Rightarrow> bool"} such that @{term"balanced n w"}
-is true iff (informally) @{text"a\<^sup>n @ w \<in> S"}. Formally, prove
-@{prop "balanced n w \<longleftrightarrow> replicate n a @ w \<in> S"} where
+is true iff (informally) @{text"S (a\<^sup>n @ w)"}. Formally, prove
+@{prop "balanced n w \<longleftrightarrow> S (replicate n a)"} where
 @{const replicate} @{text"::"} @{typ"nat \<Rightarrow> 'a \<Rightarrow> 'a list"} is predefined
 and @{term"replicate n x"} yields the list @{text"[x, \<dots>, x]"} of length @{text n}.
 \end{exercise}