src/HOL/List.thy
changeset 49962 a8cc904a6820
parent 49808 418991ce7567
child 49963 326f87427719
     1.1 --- a/src/HOL/List.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -3166,11 +3166,11 @@
     1.4  
     1.5  lemma (in monoid_add) listsum_triv:
     1.6    "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
     1.7 -  by (induct xs) (simp_all add: left_distrib)
     1.8 +  by (induct xs) (simp_all add: distrib_right)
     1.9  
    1.10  lemma (in monoid_add) listsum_0 [simp]:
    1.11    "(\<Sum>x\<leftarrow>xs. 0) = 0"
    1.12 -  by (induct xs) (simp_all add: left_distrib)
    1.13 +  by (induct xs) (simp_all add: distrib_right)
    1.14  
    1.15  text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
    1.16  lemma (in ab_group_add) uminus_listsum_map: