diff -r b730b0edc085 -r 47aa1a8fcdc9 src/HOL/HoareParallel/RG_Examples.thy
--- a/src/HOL/HoareParallel/RG_Examples.thy	Mon May 02 18:59:50 2005 +0200
+++ b/src/HOL/HoareParallel/RG_Examples.thy	Mon May 02 19:00:05 2005 +0200
@@ -154,8 +154,6 @@
 
 subsubsection {* Parameterized *}
 
-declare setsum_op_ivl_Suc [simp]
-
 lemma Example2_lemma2_aux: "j<n \<Longrightarrow> 
  (\<Sum>i=0..<n. (b i::nat)) =
  (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"