--- 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)