src/HOL/Old_Number_Theory/Finite2.thy
changeset 49962 a8cc904a6820
parent 44766 d4d33a4d7548
child 51489 f738e6dbd844
     1.1 --- a/src/HOL/Old_Number_Theory/Finite2.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri Oct 19 15:12:52 2012 +0200
     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)
     1.8 +  apply (auto simp add: distrib_right distrib_left)
     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: right_distrib)
    1.15 +  apply (auto simp add: distrib_left)
    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: right_distrib)
    1.21 +  by (induct set: finite) (auto simp add: distrib_left)
    1.22  
    1.23  
    1.24  subsection {* Cardinality of explicit finite sets *}