src/HOL/Int.thy
changeset 64267 b9a1486e79be
parent 64014 ca1239a3277b
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Int.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -866,12 +866,12 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection \<open>@{term setsum} and @{term setprod}\<close>
     1.8 +subsection \<open>@{term sum} and @{term setprod}\<close>
     1.9  
    1.10 -lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.11 +lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.12    by (induct A rule: infinite_finite_induct) auto
    1.13  
    1.14 -lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.15 +lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.16    by (induct A rule: infinite_finite_induct) auto
    1.17  
    1.18  lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.19 @@ -880,7 +880,7 @@
    1.20  lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.21    by (induct A rule: infinite_finite_induct) auto
    1.22  
    1.23 -lemmas int_setsum = of_nat_setsum [where 'a=int]
    1.24 +lemmas int_sum = of_nat_sum [where 'a=int]
    1.25  lemmas int_setprod = of_nat_setprod [where 'a=int]
    1.26  
    1.27