src/HOL/Series.thy

--- a/src/HOL/Series.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Series.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -34,7 +34,7 @@
 
 lemma sumr_diff_mult_const:
  "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
-by (simp add: diff_minus setsum_addf real_of_nat_def)
+  by (simp add: setsum_subtractf real_of_nat_def)
 
 lemma real_setsum_nat_ivl_bounded:
      "(!!p. p < n \<Longrightarrow> f(p) \<le> K)