diff -r ed574b4f7e70 -r a6b1f0cef7b3 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon Jul 12 19:56:58 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Tue Jul 13 12:32:01 2004 +0200
@@ -206,21 +206,22 @@
 
 lemma Example2_lemma2_aux2: "j\<le> s \<Longrightarrow> (\<Sum>i<j. (b (s:=t)) i) = (\<Sum>i<j. b i)"
 apply(induct j)
- apply simp_all
+ apply (simp_all cong:setsum_cong)
 done
 
-lemma Example2_lemma2: "\<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j:=1)) i)"
-apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux)
-apply(erule_tac  t="Summation (b(j := 1)) n" in ssubst)
+lemma Example2_lemma2: 
+ "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i< n. b i)=(\<Sum>i< n. (b (j := Suc 0)) i)"
+apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
+apply(erule_tac  t="setsum (b(j := (Suc 0))) {..n(}" in ssubst)
 apply(frule_tac b=b in Example2_lemma2_aux)
-apply(erule_tac  t="Summation b n" in ssubst)
-apply(subgoal_tac "Suc (Summation b j + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(Summation b j + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
- apply(rotate_tac -1)
- apply(erule ssubst)
- apply(subgoal_tac "j\<le>j")
-  apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2)
-  apply(rotate_tac -1)
-  apply(erule ssubst)
+apply(erule_tac  t="setsum b {..n(}" in ssubst)
+apply(subgoal_tac "Suc (setsum b {..j(} + b j + (\<Sum>i<n - Suc j. b (Suc j + i)))=(setsum b {..j(} + Suc (b j) + (\<Sum>i<n - Suc j. b (Suc j + i)))")
+apply(rotate_tac -1)
+apply(erule ssubst)
+apply(subgoal_tac "j\<le>j")
+ apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
+apply(rotate_tac -1)
+apply(erule ssubst)
 apply simp_all
 done