diff -r 1bbe526a552c -r 236dfafbeb63 src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Thu Jul 07 12:39:17 2005 +0200
@@ -175,12 +175,11 @@
 --{* 11 vc *}
 apply simp_all
 apply(tactic {* ALLGOALS Clarify_tac *})
---{* 11 subgoals left *}
+--{* 10 subgoals left *}
 apply(erule less_SucE)
  apply simp
 apply simp
---{* 10 subgoals left *}
-apply force
+--{* 9 subgoals left *}
 apply(case_tac "i=k")
  apply force
 apply simp
@@ -443,11 +442,11 @@
 apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
 --{* 44 subgoals left *}
 apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
---{* 33 subgoals left *}
+--{* 32 subgoals left *}
 apply(tactic {* ALLGOALS Clarify_tac *})
 
 apply(tactic {* TRYALL simple_arith_tac *})
---{* 10 subgoals left *}
+--{* 9 subgoals left *}
 apply (force simp add:less_Suc_eq)
 apply(drule sym)
 apply (force simp add:less_Suc_eq)+
@@ -525,10 +524,6 @@
 apply simp_all
 done
 
-lemma Example2_lemma3: "!!b. \<forall>i< n. b i = (Suc 0) \<Longrightarrow> (\<Sum>i=0..<n. b i)= n"
-apply (induct n)
-apply auto
-done
 
 record Example2 = 
  c :: "nat \<Rightarrow> nat" 
@@ -544,16 +539,13 @@
  COEND 
  .{\<acute>x=n}."
 apply oghoare
-apply simp_all
+apply (simp_all cong del: strong_setsum_cong)
 apply (tactic {* ALLGOALS Clarify_tac *})
-apply simp_all
-   apply(erule Example2_lemma2)
-   apply simp
-  apply(erule Example2_lemma2)
-  apply simp
- apply(erule Example2_lemma2)
- apply simp
-apply(force intro: Example2_lemma3)
+apply (simp_all cong del: strong_setsum_cong)
+   apply(erule (1) Example2_lemma2)
+  apply(erule (1) Example2_lemma2)
+ apply(erule (1) Example2_lemma2)
+apply(simp)
 done
 
 end