src/HOL/Series.thy
changeset 54230 b1d955791529
parent 53602 0ae3db699a3e
child 54703 499f92dc6e45
     1.1 --- a/src/HOL/Series.thy	Thu Oct 31 16:54:22 2013 +0100
     1.2 +++ b/src/HOL/Series.thy	Fri Nov 01 18:51:14 2013 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  lemma sumr_diff_mult_const:
     1.6   "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
     1.7 -by (simp add: diff_minus setsum_addf real_of_nat_def)
     1.8 +  by (simp add: setsum_subtractf real_of_nat_def)
     1.9  
    1.10  lemma real_setsum_nat_ivl_bounded:
    1.11       "(!!p. p < n \<Longrightarrow> f(p) \<le> K)