src/HOL/Int.thy
changeset 64272 f76b6dda2e56
parent 64267 b9a1486e79be
child 64714 53bab28983f1
     1.1 --- a/src/HOL/Int.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -866,7 +866,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -subsection \<open>@{term sum} and @{term setprod}\<close>
     1.8 +subsection \<open>@{term sum} and @{term prod}\<close>
     1.9  
    1.10  lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.11    by (induct A rule: infinite_finite_induct) auto
    1.12 @@ -874,14 +874,14 @@
    1.13  lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.14    by (induct A rule: infinite_finite_induct) auto
    1.15  
    1.16 -lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.17 +lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.18    by (induct A rule: infinite_finite_induct) auto
    1.19  
    1.20 -lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.21 +lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.22    by (induct A rule: infinite_finite_induct) auto
    1.23  
    1.24  lemmas int_sum = of_nat_sum [where 'a=int]
    1.25 -lemmas int_setprod = of_nat_setprod [where 'a=int]
    1.26 +lemmas int_prod = of_nat_prod [where 'a=int]
    1.27  
    1.28  
    1.29  text \<open>Legacy theorems\<close>