src/HOL/Old_Number_Theory/Finite2.thy
changeset 44766 d4d33a4d7548
parent 41413 64cd30d6b0b8
child 49962 a8cc904a6820
     1.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -38,18 +38,18 @@
     1.4  
     1.5  lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
     1.6    apply (induct set: finite)
     1.7 -  apply (auto simp add: left_distrib right_distrib int_eq_of_nat)
     1.8 +  apply (auto simp add: left_distrib right_distrib)
     1.9    done
    1.10  
    1.11  lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
    1.12      int(c) * int(card X)"
    1.13    apply (induct set: finite)
    1.14 -  apply (auto simp add: zadd_zmult_distrib2)
    1.15 +  apply (auto simp add: right_distrib)
    1.16    done
    1.17  
    1.18  lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
    1.19      c * setsum f A"
    1.20 -  by (induct set: finite) (auto simp add: zadd_zmult_distrib2)
    1.21 +  by (induct set: finite) (auto simp add: right_distrib)
    1.22  
    1.23  
    1.24  subsection {* Cardinality of explicit finite sets *}