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
```