src/HOL/List.thy
changeset 49963 326f87427719
parent 49948 744934b818c7
parent 49962 a8cc904a6820
child 50027 7747a9f4c358
     1.1 --- a/src/HOL/List.thy	Sun Oct 21 16:43:08 2012 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Oct 21 17:04:13 2012 +0200
     1.3 @@ -3205,11 +3205,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: