Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 49963 326f87427719
parent 49948 744934b818c7
parent 49962 a8cc904a6820
child 50027 7747a9f4c358 
--- a/src/HOL/List.thy	Sun Oct 21 16:43:08 2012 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 17:04:13 2012 +0200
@@ -3205,11 +3205,11 @@
 
 lemma (in monoid_add) listsum_triv:
   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
-  by (induct xs) (simp_all add: left_distrib)
+  by (induct xs) (simp_all add: distrib_right)
 
 lemma (in monoid_add) listsum_0 [simp]:
   "(\<Sum>x\<leftarrow>xs. 0) = 0"
-  by (induct xs) (simp_all add: left_distrib)
+  by (induct xs) (simp_all add: distrib_right)
 
 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
 lemma (in ab_group_add) uminus_listsum_map:
isabelle