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/Library/ASeries.thy
changeset 19279 48b527d0331b
parent 19109 9804aa8d5756 
--- a/src/HOL/Library/ASeries.thy	Fri Mar 17 09:57:25 2006 +0100
+++ b/src/HOL/Library/ASeries.thy	Fri Mar 17 10:04:27 2006 +0100
@@ -73,7 +73,7 @@
     by (rule setsum_addf)
   also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp
   also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))"
-    by (simp add: setsum_mult setsum_head_upt)
+    by (simp add: setsum_right_distrib setsum_head_upt)
   also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)"
     by simp
   also from ngt1 have "{1..<n} = {1..n - 1}"
isabelle