# HG changeset patch
# User nipkow
# Date 1108997865 -3600
# Node ID fa23e05614266850ce74189a46351557aa45e8aa
# Parent  333a8824456991b447db46ee075ecffb4872d5b7
removed superfluous setsum_constant

diff -r 333a88244569 -r fa23e0561426 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Mon Feb 21 15:04:10 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Mon Feb 21 15:57:45 2005 +0100
@@ -790,11 +790,6 @@
 lemma int_setprod: "int (setprod f A) = setprod (int \<circ> f) A"
   by (simp add: int_eq_of_nat setprod_of_nat)
 
-lemma setsum_constant [simp]: "finite A ==> (\<Sum>x \<in> A. y) = of_nat(card A) * y"
-  apply (erule finite_induct)
-  apply (auto simp add: ring_distrib add_ac)
-  done
-
 lemma setprod_nonzero_nat:
     "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
   by (rule setprod_nonzero, auto)