--- a/src/HOL/Old_Number_Theory/Finite2.thy Tue Sep 06 16:30:39 2011 -0700
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Tue Sep 06 19:03:41 2011 -0700
@@ -38,18 +38,18 @@
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
apply (induct set: finite)
- apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
+ apply (auto simp add: left_distrib right_distrib)
done
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
apply (induct set: finite)
- apply (auto simp add: zadd_zmult_distrib2)
+ apply (auto simp add: right_distrib)
done
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"
- by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
+ by (induct set: finite) (auto simp add: right_distrib)
subsection {* Cardinality of explicit finite sets *}