src/HOL/Groups_Big.thy
changeset 59615 fdfdf89a83a6
parent 59416 fde2659085e1
child 59833 ab828c2c5d67
     1.1 --- a/src/HOL/Groups_Big.thy	Thu Mar 05 17:39:04 2015 +0000
     1.2 +++ b/src/HOL/Groups_Big.thy	Fri Mar 06 12:48:03 2015 +0000
     1.3 @@ -953,8 +953,9 @@
     1.4  apply (auto simp add: algebra_simps)
     1.5  done
     1.6  
     1.7 -lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
     1.8 -using setsum.distrib[of f "%_. 1" A] by(simp)
     1.9 +lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
    1.10 +  using setsum.distrib[of f "\<lambda>_. 1" A] 
    1.11 +  by simp
    1.12  
    1.13  lemma setsum_bounded:
    1.14    assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"