diff -r 52a0eacf04d1 -r b6912471b8f5 src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Tue Jul 09 17:58:38 2013 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Tue Jul 09 18:08:56 2013 +0200
@@ -167,9 +167,7 @@
 
 lemma Example2_lemma2_aux2: 
   "j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
-apply(induct j)
- apply (simp_all cong:setsum_cong)
-done
+  by (induct j) simp_all
 
 lemma Example2_lemma2: 
  "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
@@ -212,7 +210,7 @@
 apply(force)
 apply clarify
 apply simp
-apply(simp cong:setsum_ivl_cong)
+apply simp
 apply clarify
 apply simp
 apply(rule Await)
@@ -228,7 +226,7 @@
 apply clarify
 apply simp
 apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
-apply simp+
+apply simp_all
 done
 
 subsection {* Find Least Element *}