--- a/src/HOL/Old_Number_Theory/Finite2.thy Fri Sep 25 23:01:34 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Wed Sep 30 17:09:12 2015 +0100
@@ -37,15 +37,11 @@
qed
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
- apply (induct set: finite)
- apply (auto simp add: distrib_right distrib_left)
- done
+by (simp add: of_nat_mult)
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
- apply (induct set: finite)
- apply (auto simp add: distrib_left)
- done
+by (simp add: of_nat_mult)
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"