# HG changeset patch
# User nipkow
# Date 1476718387 -7200
# Node ID f76b6dda2e569fefa0a5117ccf34f88fe2ae16a5
# Parent  c939cc16b605970a2f3ec7b47233ab40c9f20750
setprod -> prod

diff -r c939cc16b605 -r f76b6dda2e56 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -409,7 +409,7 @@
 @{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\
 @{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
 @{const Groups_Big.sum} & @{term_type_only Groups_Big.sum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\
-@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
+@{const Groups_Big.prod} & @{term_type_only Groups_Big.prod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
 \end{supertabular}
 
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -73,7 +73,7 @@
 qed
 
 interpretation int: comm_monoid \<Z>
-  rewrites "finprod \<Z> f A = setprod f A"
+  rewrites "finprod \<Z> f A = prod f A"
 proof -
   \<comment> "Specification"
   show "comm_monoid \<Z>" by standard auto
@@ -83,7 +83,7 @@
   { fix x y have "mult \<Z> x y = x * y" by simp }
   note mult = this
   have one: "one \<Z> = 1" by simp
-  show "finprod \<Z> f A = setprod f A"
+  show "finprod \<Z> f A = prod f A"
     by (induct A rule: infinite_finite_induct, auto)
 qed
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -3003,7 +3003,7 @@
   finally show ?thesis .
 qed
 
-lemma (in product_sigma_finite) product_integrable_setprod:
+lemma (in product_sigma_finite) product_integrable_prod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
   assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
@@ -3014,15 +3014,15 @@
     using assms by simp
   have "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) =
       (\<integral>\<^sup>+ x. (\<Prod>i\<in>I. ennreal (norm (f i (x i)))) \<partial>Pi\<^sub>M I M)"
-    by (simp add: setprod_norm setprod_ennreal)
+    by (simp add: prod_norm prod_ennreal)
   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+ x. ennreal (norm (f i x)) \<partial>M i)"
-    using assms by (intro product_nn_integral_setprod) auto
+    using assms by (intro product_nn_integral_prod) auto
   also have "\<dots> < \<infinity>"
-    using integrable by (simp add: less_top[symmetric] ennreal_setprod_eq_top integrable_iff_bounded)
+    using integrable by (simp add: less_top[symmetric] ennreal_prod_eq_top integrable_iff_bounded)
   finally show "(\<integral>\<^sup>+ x. ennreal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) < \<infinity>" .
 qed
 
-lemma (in product_sigma_finite) product_integral_setprod:
+lemma (in product_sigma_finite) product_integral_prod:
   fixes f :: "'i \<Rightarrow> 'a \<Rightarrow> _::{real_normed_field,banach,second_countable_topology}"
   assumes "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   shows "(\<integral>x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>L (M i) (f i))"
@@ -3036,10 +3036,10 @@
   then have iI: "finite (insert i I)" by auto
   then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
     integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
-    by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
+    by (intro product_integrable_prod insert(4)) (auto intro: finite_subset)
   interpret I: finite_product_sigma_finite M I by standard fact
   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
-    using \<open>i \<notin> I\<close> by (auto intro!: setprod.cong)
+    using \<open>i \<notin> I\<close> by (auto intro!: prod.cong)
   show ?case
     unfolding product_integral_insert[OF insert(1,2) prod[OF subset_refl]]
     by (simp add: * insert prod subset_insertI)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1348,7 +1348,7 @@
   shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
   using f g by (rule borel_measurable_continuous_Pair) (intro continuous_intros)
 
-lemma borel_measurable_setprod[measurable (raw)]:
+lemma borel_measurable_prod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1652,7 +1652,7 @@
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
   using assms by (induction S rule: infinite_finite_induct) auto
 
-lemma borel_measurable_ereal_setprod[measurable (raw)]:
+lemma borel_measurable_ereal_prod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
@@ -1728,7 +1728,7 @@
   shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. f x - g x) \<in> M \<rightarrow>\<^sub>M borel"
   unfolding is_borel_def[symmetric] by transfer simp
 
-lemma borel_measurable_setprod_ennreal[measurable (raw)]:
+lemma borel_measurable_prod_ennreal[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ennreal"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -37,20 +37,20 @@
 
 definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
   "det A =
-    sum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
+    sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
       {p. p permutes (UNIV :: 'n set)}"
 
 text \<open>A few general lemmas we need below.\<close>
 
-lemma setprod_permute:
+lemma prod_permute:
   assumes p: "p permutes S"
-  shows "setprod f S = setprod (f \<circ> p) S"
-  using assms by (fact setprod.permute)
+  shows "prod f S = prod (f \<circ> p) S"
+  using assms by (fact prod.permute)
 
-lemma setproduct_permute_nat_interval:
+lemma product_permute_nat_interval:
   fixes m n :: nat
-  shows "p permutes {m..n} \<Longrightarrow> setprod f {m..n} = setprod (f \<circ> p) {m..n}"
-  by (blast intro!: setprod_permute)
+  shows "p permutes {m..n} \<Longrightarrow> prod f {m..n} = prod (f \<circ> p) {m..n}"
+  by (blast intro!: prod_permute)
 
 text \<open>Basic determinant properties.\<close>
 
@@ -70,12 +70,12 @@
     have pi: "inj_on p ?U"
       by (blast intro: subset_inj_on)
     from permutes_image[OF pU]
-    have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
-      setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
+    have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
+      prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
       by simp
-    also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U"
-      unfolding setprod.reindex[OF pi] ..
-    also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
+    also have "\<dots> = prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U"
+      unfolding prod.reindex[OF pi] ..
+    also have "\<dots> = prod (\<lambda>i. ?di A i (p i)) ?U"
     proof -
       {
         fix i
@@ -84,12 +84,12 @@
         have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)"
           unfolding transpose_def by (simp add: fun_eq_iff)
       }
-      then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U =
-        setprod (\<lambda>i. ?di A i (p i)) ?U"
-        by (auto intro: setprod.cong)
+      then show "prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U =
+        prod (\<lambda>i. ?di A i (p i)) ?U"
+        by (auto intro: prod.cong)
     qed
-    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
-      of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)"
+    finally have "of_int (sign (inv p)) * (prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
+      of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)"
       using sth by simp
   }
   then show ?thesis
@@ -104,11 +104,11 @@
 lemma det_lowerdiagonal:
   fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
   assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
-  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
+  shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
 proof -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
-  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
+  let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
   have fU: "finite ?U"
     by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
@@ -123,7 +123,7 @@
       by (metis not_le)
     from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
       by blast
-    from setprod_zero[OF fU ex] have "?pp p = 0"
+    from prod_zero[OF fU ex] have "?pp p = 0"
       by simp
   }
   then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
@@ -135,11 +135,11 @@
 lemma det_upperdiagonal:
   fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
   assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
-  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
+  shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
 proof -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
-  let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
+  let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
   have fU: "finite ?U"
     by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
@@ -154,7 +154,7 @@
       by (metis not_le)
     from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
       by blast
-    from setprod_zero[OF fU ex] have "?pp p = 0"
+    from prod_zero[OF fU ex] have "?pp p = 0"
       by simp
   }
   then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
@@ -166,11 +166,11 @@
 lemma det_diagonal:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
-  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"
+  shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)"
 proof -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
-  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
+  let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
   have fU: "finite ?U" by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
   have id0: "{id} \<subseteq> ?PU"
@@ -184,7 +184,7 @@
       unfolding fun_eq_iff by auto
     from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
       by blast
-    from setprod_zero [OF fU ex] have "?pp p = 0"
+    from prod_zero [OF fU ex] have "?pp p = 0"
       by simp
   }
   then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
@@ -204,23 +204,23 @@
     have "?f i i = 1"
       using i by (vector mat_def)
   }
-  then have th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
-    by (auto intro: setprod.cong)
+  then have th: "prod (\<lambda>i. ?f i i) ?U = prod (\<lambda>x. 1) ?U"
+    by (auto intro: prod.cong)
   {
     fix i j
     assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
     have "?f i j = 0" using i j ij
       by (vector mat_def)
   }
-  then have "det ?A = setprod (\<lambda>i. ?f i i) ?U"
+  then have "det ?A = prod (\<lambda>i. ?f i i) ?U"
     using det_diagonal by blast
   also have "\<dots> = 1"
-    unfolding th setprod.neutral_const ..
+    unfolding th prod.neutral_const ..
   finally show ?thesis .
 qed
 
 lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
-  by (simp add: det_def setprod_zero)
+  by (simp add: det_def prod_zero)
 
 lemma det_permute_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
@@ -240,16 +240,16 @@
   from p q have pp: "permutation p" and qp: "permutation q"
     by (metis fU permutation_permutes)+
   from permutes_inv[OF p] have ip: "inv p permutes ?U" .
-  have "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U"
-    by (simp only: setprod_permute[OF ip, symmetric])
-  also have "\<dots> = setprod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U"
+  have "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U"
+    by (simp only: prod_permute[OF ip, symmetric])
+  also have "\<dots> = prod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U"
     by (simp only: o_def)
-  also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U"
+  also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U"
     by (simp only: o_def permutes_inverses[OF p])
-  finally have thp: "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U"
+  finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U"
     by blast
-  show "of_int (sign (q \<circ> p)) * setprod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U =
-    of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U"
+  show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U =
+    of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U"
     by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult)
 qed rule
 
@@ -341,30 +341,30 @@
     from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j"
       by simp_all
   }
-  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
-    and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk"
+  then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
+    and th2: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?h i $ p i) ?Uk"
     apply -
-    apply (rule setprod.cong, simp_all)+
+    apply (rule prod.cong, simp_all)+
     done
   have th3: "finite ?Uk" "k \<notin> ?Uk"
     by auto
-  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
+  have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
     unfolding kU[symmetric] ..
-  also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
-    apply (rule setprod.insert)
+  also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk"
+    apply (rule prod.insert)
     apply simp
     apply blast
     done
-  also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)"
+  also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?f i $ p i) ?Uk)"
     by (simp add: field_simps)
-  also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)"
+  also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?h i $ p i) ?Uk)"
     by (metis th1 th2)
-  also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
-    unfolding  setprod.insert[OF th3] by simp
-  finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U"
+  also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
+    unfolding  prod.insert[OF th3] by simp
+  finally have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?g i $ p i) ?U + prod (\<lambda>i. ?h i $ p i) ?U"
     unfolding kU[symmetric] .
-  then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
-    of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U"
+  then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U =
+    of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U"
     by (simp add: field_simps)
 qed rule
 
@@ -391,30 +391,30 @@
     from j have "?f j $ p j = ?g j $ p j"
       by simp
   }
-  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
+  then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
     apply -
-    apply (rule setprod.cong)
+    apply (rule prod.cong)
     apply simp_all
     done
   have th3: "finite ?Uk" "k \<notin> ?Uk"
     by auto
-  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
+  have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
     unfolding kU[symmetric] ..
-  also have "\<dots> = ?f k $ p k  * setprod (\<lambda>i. ?f i $ p i) ?Uk"
-    apply (rule setprod.insert)
+  also have "\<dots> = ?f k $ p k  * prod (\<lambda>i. ?f i $ p i) ?Uk"
+    apply (rule prod.insert)
     apply simp
     apply blast
     done
-  also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
+  also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk"
     by (simp add: field_simps)
-  also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
+  also have "\<dots> = c* (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk)"
     unfolding th1 by (simp add: ac_simps)
-  also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
-    unfolding setprod.insert[OF th3] by simp
-  finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
+  also have "\<dots> = c* (prod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
+    unfolding prod.insert[OF th3] by simp
+  finally have "prod (\<lambda>i. ?f i $ p i) ?U = c* (prod (\<lambda>i. ?g i $ p i) ?U)"
     unfolding kU[symmetric] .
-  then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
-    c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)"
+  then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U =
+    c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)"
     by (simp add: field_simps)
 qed rule
 
@@ -644,8 +644,8 @@
 
 lemma det_rows_mul:
   "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
-    setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
-proof (simp add: det_def sum_distrib_left cong add: setprod.cong, rule sum.cong)
+    prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
+proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong)
   let ?U = "UNIV :: 'n set"
   let ?PU = "{p. p permutes ?U}"
   fix p
@@ -653,10 +653,10 @@
   let ?s = "of_int (sign p)"
   from pU have p: "p permutes ?U"
     by blast
-  have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"
-    unfolding setprod.distrib ..
+  have "prod (\<lambda>i. c i * a i $ p i) ?U = prod c ?U * prod (\<lambda>i. a i $ p i) ?U"
+    unfolding prod.distrib ..
   then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
-    setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
+    prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
     by (simp add: field_simps)
 qed rule
 
@@ -754,17 +754,17 @@
       have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
         using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
         by (simp add:  th00 ac_simps sign_idempotent sign_compose)
-      have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
-        by (rule setprod_permute[OF p])
-      have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
-        setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U"
-        unfolding th001 setprod.distrib[symmetric] o_def permutes_inverses[OF p]
-        apply (rule setprod.cong[OF refl])
+      have th001: "prod (\<lambda>i. B$i$ q (inv p i)) ?U = prod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
+        by (rule prod_permute[OF p])
+      have thp: "prod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
+        prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U"
+        unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p]
+        apply (rule prod.cong[OF refl])
         using permutes_in_image[OF q]
         apply vector
         done
-      show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
-        ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * setprod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)"
+      show "?s q * prod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
+        ?s p * (prod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * prod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)"
         using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
         by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose)
     qed rule
@@ -1202,13 +1202,13 @@
 
 text \<open>Explicit formulas for low dimensions.\<close>
 
-lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1"
+lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1"
   by simp
 
-lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
+lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
 
-lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
+lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
 
 lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1129,7 +1129,7 @@
 
 lemma negligible_interval:
   "negligible (cbox a b) \<longleftrightarrow> box a b = {}" "negligible (box a b) \<longleftrightarrow> box a b = {}"
-   by (auto simp: negligible_iff_null_sets null_sets_def setprod_nonneg inner_diff_left box_eq_empty
+   by (auto simp: negligible_iff_null_sets null_sets_def prod_nonneg inner_diff_left box_eq_empty
                   not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
             intro: eq_refl antisym less_imp_le)
 
@@ -1254,9 +1254,9 @@
       then have ufvf: "cbox (uf X) (vf X) = X"
         using uvz by blast
       have "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i::'M \<in> Basis. prj1 (vf X - uf X))"
-        by (rule setprod_constant [symmetric])
+        by (rule prod_constant [symmetric])
       also have "\<dots> = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)"
-        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: setprod.cong)
+        using prj1_idem [OF \<open>X \<in> \<D>\<close>] by (auto simp: algebra_simps intro: prod.cong)
       finally have prj1_eq: "prj1 (vf X - uf X) ^ DIM('M) = (\<Prod>i\<in>Basis. vf X \<bullet> i - uf X \<bullet> i)" .
       have "uf X \<in> cbox (uf X) (vf X)" "vf X \<in> cbox (uf X) (vf X)"
         using uvz [OF \<open>X \<in> \<D>\<close>] by (force simp: mem_box)+
@@ -1272,7 +1272,7 @@
       have 0: "0 \<le> prj1 (vf X - uf X)"
         using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
       have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
-        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> setprod_constant)
+        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> prod_constant)
         apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
         using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
         apply (fastforce simp add: box_ne_empty power_decreasing)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -202,7 +202,7 @@
 next
   case (4 x)
   thus ?case using assms
-    by (auto intro!: setprod.cong split: if_split_asm)
+    by (auto intro!: prod.cong split: if_split_asm)
 qed
 
 
@@ -926,12 +926,12 @@
       by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
     also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) =
       (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
-      using E by (subst insert) (auto intro!: setprod.cong)
+      using E by (subst insert) (auto intro!: prod.cong)
     also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
        emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
-      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] setprod.cong)
+      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] prod.cong)
     also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
-      using insert(1,2) J E by (intro setprod.mono_neutral_right) auto
+      using insert(1,2) J E by (intro prod.mono_neutral_right) auto
     finally show "?\<mu> ?p = \<dots>" .
 
     show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))"
@@ -943,7 +943,7 @@
     show "(insert i I \<noteq> {} \<or> insert i I = {}) \<and> finite (insert i I) \<and>
       insert i I \<subseteq> insert i I \<and> A \<in> (\<Pi> j\<in>insert i I. sets (M j))"
       using insert by auto
-  qed (auto intro!: setprod.cong)
+  qed (auto intro!: prod.cong)
   with insert show ?case
     by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
 qed simp
@@ -962,7 +962,7 @@
       by (simp add: eq emeasure_PiM)
     define A where "A n = (\<Pi>\<^sub>E i\<in>I. C i n)" for n
     with C show "range A \<subseteq> prod_algebra I M" "\<And>i. emeasure (Pi\<^sub>M I M) (A i) \<noteq> \<infinity>" "(\<Union>i. A i) = space (PiM I M)"
-      by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_setprod_eq_top)
+      by (auto intro!: prod_algebraI_finite simp: emeasure_PiM subset_eq ennreal_prod_eq_top)
   qed
 qed
 
@@ -981,7 +981,7 @@
   ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets (Pi\<^sub>M I M) \<and> \<Union>A = space (Pi\<^sub>M I M) \<and> (\<forall>a\<in>A. emeasure (Pi\<^sub>M I M) a \<noteq> \<infinity>)"
     by (intro exI[of _ "PiE I ` PiE I F"])
        (auto intro!: countable_PiE sets_PiM_I_finite
-             simp: PiE_iff emeasure_PiM finite_index ennreal_setprod_eq_top)
+             simp: PiE_iff emeasure_PiM finite_index ennreal_prod_eq_top)
 qed
 
 sublocale finite_product_sigma_finite \<subseteq> sigma_finite_measure "Pi\<^sub>M I M"
@@ -1008,7 +1008,7 @@
   from A fin show "emeasure (distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J)) (Pi\<^sub>E (I \<union> J) A) =
       (\<Prod>i\<in>I \<union> J. emeasure (M i) (A i))"
     by (subst emeasure_distr)
-       (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times setprod.union_disjoint)
+       (auto simp: * J.emeasure_pair_measure_Times I.measure_times J.measure_times prod.union_disjoint)
 qed (insert fin, simp_all)
 
 lemma (in product_sigma_finite) product_nn_integral_fold:
@@ -1090,7 +1090,7 @@
   apply measurable
   done
 
-lemma (in product_sigma_finite) product_nn_integral_setprod:
+lemma (in product_sigma_finite) product_nn_integral_prod:
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> f i \<in> borel_measurable (M i)"
   shows "(\<integral>\<^sup>+ x. (\<Prod>i\<in>I. f i (x i)) \<partial>Pi\<^sub>M I M) = (\<Prod>i\<in>I. integral\<^sup>N (M i) (f i))"
 using assms proof (induction I)
@@ -1099,10 +1099,10 @@
   note \<open>finite I\<close>[intro, simp]
   interpret I: finite_product_sigma_finite M I by standard auto
   have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
-    using insert by (auto intro!: setprod.cong)
+    using insert by (auto intro!: prod.cong)
   have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)"
     using sets.sets_into_space insert
-    by (intro borel_measurable_setprod_ennreal
+    by (intro borel_measurable_prod_ennreal
               measurable_comp[OF measurable_component_singleton, unfolded comp_def])
        auto
   then show ?case
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -510,15 +510,15 @@
           (of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))"
     unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_sum)
   also from assms have "(\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))) = (\<Prod>k=1..n. z / of_nat k + 1)"
-    by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
+    by (intro prod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
   also have "... = (\<Prod>k=1..n. z + k) / fact n"
-    by (simp add: fact_setprod)
-    (subst setprod_dividef [symmetric], simp_all add: field_simps)
+    by (simp add: fact_prod)
+    (subst prod_dividef [symmetric], simp_all add: field_simps)
   also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
-    by (simp add: setprod.atLeast0_atMost_Suc_shift setprod.atLeast_Suc_atMost_Suc_shift)
+    by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift)
   also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)"
-    unfolding pochhammer_setprod
-    by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+    unfolding pochhammer_prod
+    by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
   also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
     unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
   finally show ?thesis .
@@ -995,10 +995,10 @@
                         norm (y - z)) (nhds 0) (at z)"
   assumes differentiable_rGamma_aux2:
     "let z = - of_nat n
-     in  filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (setprod of_nat {1..n}) * (y - z)) /\<^sub>R
+     in  filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (prod of_nat {1..n}) * (y - z)) /\<^sub>R
                         norm (y - z)) (nhds 0) (at z)"
   assumes rGamma_series_aux: "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow>
-             let fact' = (\<lambda>n. setprod of_nat {1..n});
+             let fact' = (\<lambda>n. prod of_nat {1..n});
                  exp = (\<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x^k /\<^sub>R fact k) \<longlonglongrightarrow> e);
                  pochhammer' = (\<lambda>a n. (\<Prod>n = 0..n. a + of_nat n))
              in  filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1))))
@@ -1033,7 +1033,7 @@
   case False
   hence "z \<noteq> - of_nat n" for n by auto
   from rGamma_series_aux[OF this] show ?thesis
-    by (simp add: rGamma_series_def[abs_def] fact_setprod pochhammer_Suc_setprod
+    by (simp add: rGamma_series_def[abs_def] fact_prod pochhammer_Suc_prod
                   exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
 qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
 
@@ -1183,7 +1183,7 @@
   apply (rule has_field_derivative_at_within)
   using differentiable_rGamma_aux2[of n]
   unfolding Let_def has_field_derivative_def has_derivative_def netlimit_at
-  by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_setprod) simp
+  by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_prod) simp
 
 lemma has_field_derivative_rGamma [derivative_intros]:
   "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>norm z\<rfloor>) * fact (nat \<lfloor>norm z\<rfloor>)
@@ -1387,18 +1387,18 @@
 next
   fix n :: nat
   from has_field_derivative_rGamma_complex_nonpos_Int[of n]
-  show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * setprod of_nat {1..n} *
+  show "let z = - of_nat n in (\<lambda>y. (rGamma y - rGamma z - (- 1) ^ n * prod of_nat {1..n} *
                   (y - z)) /\<^sub>R cmod (y - z)) \<midarrow>z\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
 next
   fix z :: complex
   from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z"
     by (simp add: convergent_LIMSEQ_iff rGamma_complex_def)
-  thus "let fact' = \<lambda>n. setprod of_nat {1..n};
+  thus "let fact' = \<lambda>n. prod of_nat {1..n};
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
-    by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+    by (simp add: fact_prod pochhammer_Suc_prod rGamma_series_def [abs_def] exp_def
                   of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
@@ -1517,9 +1517,9 @@
   have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
     by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
-  thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * setprod of_nat {1..n} *
+  thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * prod of_nat {1..n} *
                   (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
-    by (simp add: has_field_derivative_def has_derivative_def fact_setprod netlimit_at Let_def)
+    by (simp add: has_field_derivative_def has_derivative_def fact_prod netlimit_at Let_def)
 next
   fix x :: real
   have "rGamma_series x \<longlonglongrightarrow> rGamma x"
@@ -1527,11 +1527,11 @@
     show "(\<lambda>n. Re (rGamma_series (of_real x) n)) \<longlonglongrightarrow> rGamma x" unfolding rGamma_real_def
       by (intro tendsto_intros)
   qed (insert rGamma_series_real, simp add: eq_commute)
-  thus "let fact' = \<lambda>n. setprod of_nat {1..n};
+  thus "let fact' = \<lambda>n. prod of_nat {1..n};
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
-    by (simp add: fact_setprod pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
+    by (simp add: fact_prod pochhammer_Suc_prod rGamma_series_def [abs_def] exp_def
                   of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
@@ -2575,11 +2575,11 @@
           exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))"
     by (subst exp_sum [symmetric]) (simp_all add: sum_distrib_left)
   also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)"
-    by (subst ln_setprod [symmetric]) (auto intro!: add_pos_nonneg)
+    by (subst ln_prod [symmetric]) (auto intro!: add_pos_nonneg)
   also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
-    by (intro setprod.cong) (simp_all add: divide_simps)
+    by (intro prod.cong) (simp_all add: divide_simps)
   also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
-    by (induction n) (simp_all add: setprod_nat_ivl_Suc' divide_simps)
+    by (induction n) (simp_all add: prod_nat_ivl_Suc' divide_simps)
   finally show ?thesis ..
 qed
 
@@ -2606,11 +2606,11 @@
     from n z' have "Gamma_series_euler' z n =
       exp (z * of_real (ln (of_nat n + 1))) / (z * (\<Prod>k=1..n. (1 + z / of_nat k)))"
       by (subst Gamma_euler'_aux1)
-         (simp_all add: Gamma_series_euler'_def setprod.distrib
-                        setprod_inversef[symmetric] divide_inverse)
+         (simp_all add: Gamma_series_euler'_def prod.distrib
+                        prod_inversef[symmetric] divide_inverse)
     also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
-      by (cases n) (simp_all add: pochhammer_setprod fact_setprod atLeastLessThanSuc_atLeastAtMost
-        setprod_dividef [symmetric] field_simps setprod.atLeast_Suc_atMost_Suc_shift)
+      by (cases n) (simp_all add: pochhammer_prod fact_prod atLeastLessThanSuc_atLeastAtMost
+        prod_dividef [symmetric] field_simps prod.atLeast_Suc_atMost_Suc_shift)
     also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
     finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
   qed
@@ -2681,7 +2681,7 @@
   case False
   have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
     by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
-                  exp_minus divide_inverse setprod_inversef[symmetric] mult_ac)
+                  exp_minus divide_inverse prod_inversef[symmetric] mult_ac)
   also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
     by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
   finally show ?thesis by (simp add: Gamma_def)
@@ -2865,7 +2865,7 @@
       also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
       also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
         by (simp add: divide_simps pochhammer_rec
-              setprod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
+              prod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
       finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
         by simp
     qed (simp_all add: bounded_bilinear_mult)
@@ -3024,10 +3024,10 @@
     have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
               of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
       by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
-                    divide_simps setprod.distrib[symmetric] power2_eq_square)
+                    divide_simps prod.distrib[symmetric] power2_eq_square)
     also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
                  (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
-      by (intro setprod.cong) (simp_all add: power2_eq_square field_simps)
+      by (intro prod.cong) (simp_all add: power2_eq_square field_simps)
     finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \<dots>"
       by (simp add: divide_simps)
   qed
@@ -3058,10 +3058,10 @@
   from tendsto_inverse[OF tendsto_mult[OF 
          sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
     have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2" 
-    by (simp add: setprod_inversef [symmetric])
+    by (simp add: prod_inversef [symmetric])
   also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
                (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
-    by (intro ext setprod.cong refl) (simp add: divide_simps)
+    by (intro ext prod.cong refl) (simp add: divide_simps)
   finally show ?thesis .
 qed
 
@@ -3086,7 +3086,7 @@
     have "(\<lambda>n. P x n - P x (Suc n)) sums (P x 0 - sin (pi * x) / (pi * x))"
       unfolding P_def using x by (intro telescope_sums' sin_product_formula_real')
     also have "(\<lambda>n. P x n - P x (Suc n)) = (\<lambda>n. (x^2 / of_nat (Suc n)^2) * P x n)"
-      unfolding P_def by (simp add: setprod_nat_ivl_Suc' algebra_simps)
+      unfolding P_def by (simp add: prod_nat_ivl_Suc' algebra_simps)
     also have "P x 0 = 1" by (simp add: P_def)
     finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" .
     from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp
@@ -3104,9 +3104,9 @@
         finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k
           by (simp_all add: field_simps del: of_nat_Suc)
       }
-      hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro setprod_mono) simp
+      hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro prod_mono) simp
       thus "norm (P x n / (of_nat (Suc n)^2)) \<le> 1 / of_nat (Suc n)^2"
-        unfolding P_def by (simp add: field_simps abs_setprod del: of_nat_Suc)
+        unfolding P_def by (simp add: field_simps abs_prod del: of_nat_Suc)
     qed (subst summable_Suc_iff, insert inverse_power_summable[of 2], simp add: inverse_eq_divide)
   qed (auto simp: P_def intro!: continuous_intros)
   hence "isCont f 0" by (subst (asm) continuous_on_eq_continuous_at) simp_all
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Generalised_Binomial_Theorem.thy
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -31,9 +31,9 @@
     let ?P = "\<Prod>i=0..<n. a - of_nat i"
     from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
                    (?P / (\<Prod>i=0..n. a - of_nat i))"
-      by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+      by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
     also from q have "(\<Prod>i=0..n. a - of_nat i) = ?P * (a - of_nat n)"
-      by (simp add: setprod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
+      by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
     also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
     also from assms have "?P / ?P = 1" by auto
     also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
@@ -210,7 +210,7 @@
   also have "(of_real (1 + z) :: complex) powr (of_real a) = of_real ((1 + z) powr a)"
     using assms by (subst powr_of_real) simp_all
   also have "(of_real a gchoose n :: complex) = of_real (a gchoose n)" for n
-    by (simp add: gbinomial_setprod_rev)
+    by (simp add: gbinomial_prod_rev)
   hence "(\<lambda>n. (of_real a gchoose n :: complex) * of_real z ^ n) =
            (\<lambda>n. of_real ((a gchoose n) * z ^ n))" by (intro ext) simp
   finally show ?thesis by (simp only: sums_of_real_iff)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -56,7 +56,7 @@
   where "content s \<equiv> measure lborel s"
 
 lemma content_cbox_cases:
-  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
+  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then prod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
   by (simp add: measure_lborel_cbox_eq inner_diff)
 
 lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
@@ -84,7 +84,7 @@
   using not_le by blast
 
 lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
-  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
+  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: prod_pos)
 
 lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
   by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
@@ -93,7 +93,7 @@
   unfolding content_eq_0 interior_cbox box_eq_empty by auto
 
 lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
-  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
+  by (auto simp add: content_cbox_cases less_le prod_nonneg)
 
 lemma content_empty [simp]: "content {} = 0"
   by simp
@@ -110,9 +110,9 @@
 
 lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
   unfolding measure_lborel_cbox_eq Basis_prod_def
-  apply (subst setprod.union_disjoint)
+  apply (subst prod.union_disjoint)
   apply (auto simp: bex_Un ball_Un)
-  apply (subst (1 2) setprod.reindex_nontrivial)
+  apply (subst (1 2) prod.reindex_nontrivial)
   apply auto
   done
 
@@ -138,7 +138,7 @@
     apply (subst *(1))
     defer
     apply (subst *(1))
-    unfolding setprod.insert[OF *(2-)]
+    unfolding prod.insert[OF *(2-)]
     apply auto
     done
   assume as: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
@@ -151,7 +151,7 @@
       (\<Prod>i\<in>Basis. (if i = k then min (b \<bullet> k) c else b \<bullet> i) - a \<bullet> i)"
     "(\<Prod>i\<in>Basis. b \<bullet> i - ((\<Sum>i\<in>Basis. (if i = k then max (a \<bullet> k) c else a \<bullet> i) *\<^sub>R i) \<bullet> i)) =
       (\<Prod>i\<in>Basis. b \<bullet> i - (if i = k then max (a \<bullet> k) c else a \<bullet> i))"
-    by (auto intro!: setprod.cong)
+    by (auto intro!: prod.cong)
   have "\<not> a \<bullet> k \<le> c \<Longrightarrow> \<not> c \<le> b \<bullet> k \<Longrightarrow> False"
     unfolding not_le
     using as[unfolded ,rule_format,of k] assms
@@ -1876,7 +1876,7 @@
     by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
   also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
     using k *
-    by (intro setprod_zero bexI[OF _ k])
+    by (intro prod_zero bexI[OF _ k])
        (auto simp: b'_def a'_def inner_diff inner_sum_left inner_not_same_Basis intro!: sum.cong)
   also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
     ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
@@ -3472,7 +3472,7 @@
   also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
     by (intro measure_times) auto
   also have "\<dots> = 0"
-    by (intro setprod_zero bexI[OF _ k]) auto
+    by (intro prod_zero bexI[OF _ k]) auto
   finally show ?thesis
     by (subst AE_iff_measurable[OF _ refl]) auto
 qed
@@ -3494,13 +3494,13 @@
   show ?thesis
     using m unfolding eq measure_def
     by (subst lborel_affine_euclidean[where c=m and t=0])
-       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
-                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
+       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_prod nn_integral_cmult
+                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult prod_nonneg)
 next
   assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
   then obtain k where k: "k \<in> Basis" "m k = 0" by auto
   then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
-    by (intro setprod_zero) auto
+    by (intro prod_zero) auto
   have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
   proof (rule emeasure_eq_0_AE)
     show "AE x in lborel. x \<notin> s m ` cbox a b"
@@ -3539,7 +3539,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis
       by (simp add: image_affinity_cbox True content_cbox'
-        setprod.distrib setprod_constant inner_diff_left)
+        prod.distrib prod_constant inner_diff_left)
   next
     case False
     with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
@@ -3552,7 +3552,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis using False
       by (simp add: image_affinity_cbox content_cbox'
-        setprod.distrib[symmetric] setprod_constant[symmetric] inner_diff_left)
+        prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left)
   qed
 qed
 
@@ -3589,7 +3589,7 @@
   assumes "(f has_integral i) (cbox a b)"
     and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
-         ((1/ \<bar>setprod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
+         ((1/ \<bar>prod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
 apply (rule has_integral_twiddle[where f=f])
 unfolding zero_less_abs_iff content_image_stretch_interval
 unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
@@ -7371,7 +7371,8 @@
 subsection \<open>Integration by parts\<close>
 
 lemma integration_by_parts_interior_strong:
-  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes bilinear: "bounded_bilinear (prod)"
   assumes s: "finite s" and le: "a \<le> b"
   assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
@@ -7389,7 +7390,8 @@
 qed
 
 lemma integration_by_parts_interior:
-  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes "bounded_bilinear (prod)" "a \<le> b"
           "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
           "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7398,7 +7400,8 @@
   by (rule integration_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
 
 lemma integration_by_parts:
-  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes "bounded_bilinear (prod)" "a \<le> b"
           "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
           "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7407,7 +7410,8 @@
   by (rule integration_by_parts_interior[of _ _ _ f g f' g']) (insert assms, simp_all)
 
 lemma integrable_by_parts_interior_strong:
-  assumes bilinear: "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes bilinear: "bounded_bilinear (prod)"
   assumes s: "finite s" and le: "a \<le> b"
   assumes cont [continuous_intros]: "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes deriv: "\<And>x. x\<in>{a<..<b} - s \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
@@ -7424,7 +7428,8 @@
 qed
 
 lemma integrable_by_parts_interior:
-  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes "bounded_bilinear (prod)" "a \<le> b"
           "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
           "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
@@ -7433,7 +7438,8 @@
   by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)
 
 lemma integrable_by_parts:
-  assumes "bounded_bilinear (prod :: _ \<Rightarrow> _ \<Rightarrow> 'b :: banach)" "a \<le> b"
+  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
+  assumes "bounded_bilinear (prod)" "a \<le> b"
           "continuous_on {a..b} f" "continuous_on {a..b} g"
   assumes "\<And>x. x\<in>{a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
           "\<And>x. x\<in>{a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -404,11 +404,11 @@
 lemma lborel_eq: "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. lborel) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
   by (subst lborel_def) (simp add: lborel_eq_real)
 
-lemma nn_integral_lborel_setprod:
+lemma nn_integral_lborel_prod:
   assumes [measurable]: "\<And>b. b \<in> Basis \<Longrightarrow> f b \<in> borel_measurable borel"
   assumes nn[simp]: "\<And>b x. b \<in> Basis \<Longrightarrow> 0 \<le> f b x"
   shows "(\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. f b (x \<bullet> b)) \<partial>lborel) = (\<Prod>b\<in>Basis. (\<integral>\<^sup>+x. f b x \<partial>lborel))"
-  by (simp add: lborel_def nn_integral_distr product_nn_integral_setprod
+  by (simp add: lborel_def nn_integral_distr product_nn_integral_prod
                 product_nn_integral_singleton)
 
 lemma emeasure_lborel_Icc[simp]:
@@ -434,13 +434,13 @@
   then have "emeasure lborel (cbox l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b .. u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
     by simp
   also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
-    by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left)
+    by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
   finally show ?thesis .
 qed
 
 lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
   using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
-  by (auto simp add: cbox_sing setprod_constant power_0_left)
+  by (auto simp add: cbox_sing prod_constant power_0_left)
 
 lemma emeasure_lborel_Ioo[simp]:
   assumes [simp]: "l \<le> u"
@@ -481,7 +481,7 @@
   then have "emeasure lborel (box l u) = (\<integral>\<^sup>+x. (\<Prod>b\<in>Basis. indicator {l\<bullet>b <..< u\<bullet>b} (x \<bullet> b)) \<partial>lborel)"
     by simp
   also have "\<dots> = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
-    by (subst nn_integral_lborel_setprod) (simp_all add: setprod_ennreal inner_diff_left)
+    by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
   finally show ?thesis .
 qed
 
@@ -495,7 +495,7 @@
 
 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
   using emeasure_lborel_cbox[of x x] nonempty_Basis
-  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
+  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing prod_constant)
 
 lemma
   fixes l u :: real
@@ -510,7 +510,7 @@
   assumes [simp]: "\<And>b. b \<in> Basis \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
   shows measure_lborel_box[simp]: "measure lborel (box l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
     and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
-  by (simp_all add: measure_def inner_diff_left setprod_nonneg)
+  by (simp_all add: measure_def inner_diff_left prod_nonneg)
 
 lemma measure_lborel_cbox_eq:
   "measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
@@ -549,7 +549,7 @@
   show ?thesis
     unfolding UN_box_eq_UNIV[symmetric]
     apply (subst SUP_emeasure_incseq[symmetric])
-    apply (auto simp: incseq_def subset_box inner_add_left setprod_constant
+    apply (auto simp: incseq_def subset_box inner_add_left prod_constant
       simp del: Sup_eq_top_iff SUP_eq_top_iff
       intro!: ennreal_SUP_eq_top)
     done
@@ -629,15 +629,15 @@
     using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
   with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
     by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
-                   field_simps divide_simps ennreal_mult'[symmetric] setprod_nonneg setprod.distrib[symmetric]
-             intro!: setprod.cong)
+                   field_simps divide_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric]
+             intro!: prod.cong)
 qed simp
 
 lemma lborel_affine:
   fixes t :: "'a::euclidean_space"
   shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
   using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
-  unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation setprod_constant by simp
+  unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation prod_constant by simp
 
 lemma lborel_real_affine:
   "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
@@ -696,7 +696,7 @@
     then have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))) A = 0"
       unfolding T_def using c by (subst lborel_affine_euclidean[symmetric]) auto
     also have "\<dots> \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0"
-      using A c by (simp add: distr_completion emeasure_density nn_integral_cmult setprod_nonneg cong: distr_cong)
+      using A c by (simp add: distr_completion emeasure_density nn_integral_cmult prod_nonneg cong: distr_cong)
     finally have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0" . }
   then have eq: "null_sets lborel = null_sets (distr lebesgue lborel T)"
     by (auto simp: null_sets_def)
@@ -707,7 +707,7 @@
   have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))"
     using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
   also have "\<dots> = density (completion (distr lebesgue lborel T)) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
-    using c by (auto intro!: always_eventually setprod_pos completion_density_eq simp: distr_completion cong: distr_cong)
+    using c by (auto intro!: always_eventually prod_pos completion_density_eq simp: distr_completion cong: distr_cong)
   also have "\<dots> = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
     by (subst completion.completion_distr_eq) (auto simp: eq measurable_completion)
   finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
@@ -761,7 +761,7 @@
         apply (subst lebesgue_affine_euclidean[of "\<lambda>_. m" \<delta>])
         apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr
                         del: space_completion emeasure_completion)
-        apply (simp add: vimage_comp s_comp_s setprod_constant)
+        apply (simp add: vimage_comp s_comp_s prod_constant)
         done
     next
       assume "S \<notin> sets lebesgue"
@@ -779,7 +779,7 @@
     qed
   qed
   show ?m
-    unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult setprod_nonneg)
+    unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
 qed
 
 lemma divideR_right:
@@ -843,9 +843,9 @@
     "box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
     using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
   show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
-      ennreal (setprod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
-    by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def setprod.union_disjoint
-                  setprod.reindex ennreal_mult inner_diff_left setprod_nonneg)
+      ennreal (prod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+    by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint
+                  prod.reindex ennreal_mult inner_diff_left prod_nonneg)
 qed (simp add: borel_prod[symmetric])
 
 (* FIXME: conversion in measurable prover *)
@@ -860,7 +860,7 @@
   then have "emeasure lborel A \<le> emeasure lborel (cbox a b)"
     by (intro emeasure_mono) auto
   then show ?thesis
-    by (auto simp: emeasure_lborel_cbox_eq setprod_nonneg less_top[symmetric] top_unique split: if_split_asm)
+    by (auto simp: emeasure_lborel_cbox_eq prod_nonneg less_top[symmetric] top_unique split: if_split_asm)
 qed
 
 lemma emeasure_compact_finite: "compact A \<Longrightarrow> emeasure lborel A < \<infinity>"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -192,7 +192,7 @@
   lemma sum: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>i \<in> I. f i x) \<in> R"
     by (induct I rule: finite_induct; simp add: const add)
 
-  lemma setprod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
+  lemma prod: "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i \<in> R\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Prod>i \<in> I. f i x) \<in> R"
     by (induct I rule: finite_induct; simp add: const mult)
 
   definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
@@ -467,19 +467,19 @@
     by metis
   define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x
   have pffR: "pff \<in> R"
-    unfolding pff_def using subA ff by (auto simp: intro: setprod)
+    unfolding pff_def using subA ff by (auto simp: intro: prod)
   moreover
   have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x
   proof -
     have "0 \<le> pff x"
       using subA cardp t
       apply (simp add: pff_def divide_simps sum_nonneg)
-      apply (rule Groups_Big.linordered_semidom_class.setprod_nonneg)
+      apply (rule Groups_Big.linordered_semidom_class.prod_nonneg)
       using ff by fastforce
     moreover have "pff x \<le> 1"
       using subA cardp t
       apply (simp add: pff_def divide_simps sum_nonneg)
-      apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified])
+      apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
       using ff by fastforce
     ultimately show ?thesis
       by auto
@@ -488,10 +488,10 @@
   { fix v x
     assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> S"
     from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)"
-      unfolding pff_def  by (metis setprod.remove)
+      unfolding pff_def  by (metis prod.remove)
     also have "... \<le> ff v x * 1"
       apply (rule Rings.ordered_semiring_class.mult_left_mono)
-      apply (rule setprod_mono [where g = "\<lambda>x. 1", simplified])
+      apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
       using ff [THEN conjunct2, THEN conjunct1] v subA x
       apply auto
       apply (meson atLeastAtMost_iff contra_subsetD imageI)
@@ -515,10 +515,10 @@
       using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp
       by (auto simp: field_simps)
     also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)"
-      by (simp add: setprod_constant subA(2))
+      by (simp add: prod_constant subA(2))
     also have "... < pff x"
       apply (simp add: pff_def)
-      apply (rule setprod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
+      apply (rule prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
       apply (simp_all add: subA(2))
       apply (intro ballI conjI)
       using e apply (force simp: divide_simps)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Analysis/ex/Approximations.thy
--- a/src/HOL/Analysis/ex/Approximations.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Analysis/ex/Approximations.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -185,12 +185,12 @@
   also have "\<dots> = (\<Sum>k\<le>n. 1 / fact k)"
   proof (intro sum.cong refl)
     fix k assume k: "k \<in> {..n}"
-    have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_setprod)
+    have "fact n = (\<Prod>i=1..n. real i)" by (simp add: fact_prod)
     also from k have "{1..n} = {1..k} \<union> {k+1..n}" by auto
-    also have "setprod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
-      by (subst nonzero_divide_eq_eq, simp, subst setprod.union_disjoint [symmetric]) auto
-    also have "\<dots> = fact k" by (simp add: fact_setprod)
-    finally show "1 / (fact n / setprod real {k + 1..n}) = 1 / fact k" by simp
+    also have "prod real \<dots> / (\<Prod>i=k+1..n. real i) = (\<Prod>i=1..k. real i)"
+      by (subst nonzero_divide_eq_eq, simp, subst prod.union_disjoint [symmetric]) auto
+    also have "\<dots> = fact k" by (simp add: fact_prod)
+    finally show "1 / (fact n / prod real {k + 1..n}) = 1 / fact k" by simp
   qed
   also have "\<dots> = euler_approx n" by (simp add: euler_approx_def field_simps)
   finally show ?thesis by (simp add: euler_approx_aux_def)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Binomial.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -18,45 +18,45 @@
 begin
 
 definition fact :: "nat \<Rightarrow> 'a"
-  where fact_setprod: "fact n = of_nat (\<Prod>{1..n})"
+  where fact_prod: "fact n = of_nat (\<Prod>{1..n})"
 
-lemma fact_setprod_Suc: "fact n = of_nat (setprod Suc {0..<n})"
+lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
   by (cases n)
-    (simp_all add: fact_setprod setprod.atLeast_Suc_atMost_Suc_shift
+    (simp_all add: fact_prod prod.atLeast_Suc_atMost_Suc_shift
       atLeastLessThanSuc_atLeastAtMost)
 
-lemma fact_setprod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
-  using setprod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
+lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
+  using prod.atLeast_atMost_rev [of "\<lambda>i. i" 1 n]
   by (cases n)
-    (simp_all add: fact_setprod_Suc setprod.atLeast_Suc_atMost_Suc_shift
+    (simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
       atLeastLessThanSuc_atLeastAtMost)
 
 lemma fact_0 [simp]: "fact 0 = 1"
-  by (simp add: fact_setprod)
+  by (simp add: fact_prod)
 
 lemma fact_1 [simp]: "fact 1 = 1"
-  by (simp add: fact_setprod)
+  by (simp add: fact_prod)
 
 lemma fact_Suc_0 [simp]: "fact (Suc 0) = 1"
-  by (simp add: fact_setprod)
+  by (simp add: fact_prod)
 
 lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
-  by (simp add: fact_setprod atLeastAtMostSuc_conv algebra_simps)
+  by (simp add: fact_prod atLeastAtMostSuc_conv algebra_simps)
 
 lemma fact_2 [simp]: "fact 2 = 2"
   by (simp add: numeral_2_eq_2)
 
-lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (setprod Suc {n - k..<n}) * fact (n - k)"
-  by (simp add: fact_setprod_Suc setprod.union_disjoint [symmetric]
+lemma fact_split: "k \<le> n \<Longrightarrow> fact n = of_nat (prod Suc {n - k..<n}) * fact (n - k)"
+  by (simp add: fact_prod_Suc prod.union_disjoint [symmetric]
     ivl_disj_un ac_simps of_nat_mult [symmetric])
 
 end
 
 lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
-  by (simp add: fact_setprod)
+  by (simp add: fact_prod)
 
 lemma of_int_fact [simp]: "of_int (fact n) = fact n"
-  by (simp only: fact_setprod of_int_of_nat_eq)
+  by (simp only: fact_prod of_int_of_nat_eq)
 
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto
@@ -170,7 +170,7 @@
   shows "fact n div fact (n - r) \<le> n ^ r"
 proof -
   have "r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}" for r
-    by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
+    by (subst prod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
   with assms show ?thesis
     by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
 qed
@@ -434,7 +434,7 @@
   with True have "n = m + 2"
     by simp
   then have "fact n = n * (n - 1) * fact (n - 2)"
-    by (simp add: fact_setprod_Suc atLeast0_lessThan_Suc algebra_simps)
+    by (simp add: fact_prod_Suc atLeast0_lessThan_Suc algebra_simps)
   with True show ?thesis
     by (simp add: binomial_fact')
 qed
@@ -508,29 +508,29 @@
 begin
 
 definition pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
-  where pochhammer_setprod: "pochhammer a n = setprod (\<lambda>i. a + of_nat i) {0..<n}"
+  where pochhammer_prod: "pochhammer a n = prod (\<lambda>i. a + of_nat i) {0..<n}"
 
-lemma pochhammer_setprod_rev: "pochhammer a n = setprod (\<lambda>i. a + of_nat (n - i)) {1..n}"
-  using setprod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
-  by (simp add: pochhammer_setprod)
+lemma pochhammer_prod_rev: "pochhammer a n = prod (\<lambda>i. a + of_nat (n - i)) {1..n}"
+  using prod.atLeast_lessThan_rev_at_least_Suc_atMost [of "\<lambda>i. a + of_nat i" 0 n]
+  by (simp add: pochhammer_prod)
 
-lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat i) {0..n}"
-  by (simp add: pochhammer_setprod atLeastLessThanSuc_atLeastAtMost)
+lemma pochhammer_Suc_prod: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat i) {0..n}"
+  by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)
 
-lemma pochhammer_Suc_setprod_rev: "pochhammer a (Suc n) = setprod (\<lambda>i. a + of_nat (n - i)) {0..n}"
-  by (simp add: pochhammer_setprod_rev setprod.atLeast_Suc_atMost_Suc_shift)
+lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
+  by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift)
 
 lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
-  by (simp add: pochhammer_setprod)
+  by (simp add: pochhammer_prod)
 
 lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
-  by (simp add: pochhammer_setprod lessThan_Suc)
+  by (simp add: pochhammer_prod lessThan_Suc)
 
 lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
-  by (simp add: pochhammer_setprod lessThan_Suc)
+  by (simp add: pochhammer_prod lessThan_Suc)
 
 lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
-  by (simp add: pochhammer_setprod atLeast0_lessThan_Suc ac_simps)
+  by (simp add: pochhammer_prod atLeast0_lessThan_Suc ac_simps)
 
 end
 
@@ -545,22 +545,22 @@
   by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
 
 lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
-  by (simp add: pochhammer_setprod)
+  by (simp add: pochhammer_prod)
 
 lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
-  by (simp add: pochhammer_setprod)
+  by (simp add: pochhammer_prod)
 
 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
-  by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc_shift ac_simps)
+  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
 
 lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
-  by (simp add: pochhammer_setprod setprod.atLeast0_lessThan_Suc ac_simps)
+  by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)
 
 lemma pochhammer_fact: "fact n = pochhammer 1 n"
-  by (simp add: pochhammer_setprod fact_setprod_Suc)
+  by (simp add: pochhammer_prod fact_prod_Suc)
 
 lemma pochhammer_of_nat_eq_0_lemma: "k > n \<Longrightarrow> pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
-  by (auto simp add: pochhammer_setprod)
+  by (auto simp add: pochhammer_prod)
 
 lemma pochhammer_of_nat_eq_0_lemma':
   assumes kn: "k \<le> n"
@@ -571,7 +571,7 @@
 next
   case (Suc h)
   then show ?thesis
-    apply (simp add: pochhammer_Suc_setprod)
+    apply (simp add: pochhammer_Suc_prod)
     using Suc kn
     apply (auto simp add: algebra_simps)
     done
@@ -585,7 +585,7 @@
   by (auto simp add: not_le[symmetric])
 
 lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
-  by (auto simp add: pochhammer_setprod eq_neg_iff_add_eq_0)
+  by (auto simp add: pochhammer_prod eq_neg_iff_add_eq_0)
 
 lemma pochhammer_eq_0_mono:
   "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
@@ -603,11 +603,11 @@
 next
   case (Suc h)
   have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i = 0..h. - 1)"
-    using setprod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
+    using prod_constant [where A="{0.. h}" and y="- 1 :: 'a"]
     by auto
   with Suc show ?thesis
-    using pochhammer_Suc_setprod_rev [of "b - of_nat k + 1"]
-    by (auto simp add: pochhammer_Suc_setprod setprod.distrib [symmetric] eq of_nat_diff)
+    using pochhammer_Suc_prod_rev [of "b - of_nat k + 1"]
+    by (auto simp add: pochhammer_Suc_prod prod.distrib [symmetric] eq of_nat_diff)
 qed
 
 lemma pochhammer_minus':
@@ -705,19 +705,19 @@
 subsection \<open>Generalized binomial coefficients\<close>
 
 definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "gchoose" 65)
-  where gbinomial_setprod_rev: "a gchoose n = setprod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
+  where gbinomial_prod_rev: "a gchoose n = prod (\<lambda>i. a - of_nat i) {0..<n} div fact n"
 
 lemma gbinomial_0 [simp]:
   "a gchoose 0 = 1"
   "0 gchoose (Suc n) = 0"
-  by (simp_all add: gbinomial_setprod_rev setprod.atLeast0_lessThan_Suc_shift)
+  by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift)
 
-lemma gbinomial_Suc: "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
-  by (simp add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
+  by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
 
 lemma gbinomial_mult_fact: "fact n * (a gchoose n) = (\<Prod>i = 0..<n. a - of_nat i)"
   for a :: "'a::field_char_0"
-  by (simp_all add: gbinomial_setprod_rev field_simps)
+  by (simp_all add: gbinomial_prod_rev field_simps)
 
 lemma gbinomial_mult_fact': "(a gchoose n) * fact n = (\<Prod>i = 0..<n. a - of_nat i)"
   for a :: "'a::field_char_0"
@@ -727,9 +727,9 @@
   for a :: "'a::field_char_0"
   by (cases n)
     (simp_all add: pochhammer_minus,
-     simp_all add: gbinomial_setprod_rev pochhammer_setprod_rev
+     simp_all add: gbinomial_prod_rev pochhammer_prod_rev
        power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
-       setprod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
+       prod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
 
 lemma gbinomial_pochhammer': "s gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
   for s :: "'a::field_char_0"
@@ -749,42 +749,42 @@
     by (simp add: not_le)
   then have "0 \<in> (op - n) ` {0..<k}"
     by auto
-  then have "setprod (op - n) {0..<k} = 0"
-    by (auto intro: setprod_zero)
+  then have "prod (op - n) {0..<k} = 0"
+    by (auto intro: prod_zero)
   with \<open>n < k\<close> show ?thesis
-    by (simp add: binomial_eq_0 gbinomial_setprod_rev setprod_zero)
+    by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero)
 next
   case True
   then have "inj_on (op - n) {0..<k}"
     by (auto intro: inj_onI)
-  then have "\<Prod>(op - n ` {0..<k}) = setprod (op - n) {0..<k}"
-    by (auto dest: setprod.reindex)
+  then have "\<Prod>(op - n ` {0..<k}) = prod (op - n) {0..<k}"
+    by (auto dest: prod.reindex)
   also have "op - n ` {0..<k} = {Suc (n - k)..n}"
     using True by (auto simp add: image_def Bex_def) presburger  (* FIXME slow *)
-  finally have *: "setprod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
+  finally have *: "prod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
   from True have "n choose k = fact n div (fact k * fact (n - k))"
     by (rule binomial_fact')
   with * show ?thesis
-    by (simp add: gbinomial_setprod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
+    by (simp add: gbinomial_prod_rev mult.commute [of "fact k"] div_mult2_eq fact_div_fact)
 qed
 
 lemma of_nat_gbinomial: "of_nat (n gchoose k) = (of_nat n gchoose k :: 'a::field_char_0)"
 proof (cases "k \<le> n")
   case False
   then show ?thesis
-    by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_setprod_rev)
+    by (simp add: not_le gbinomial_binomial binomial_eq_0 gbinomial_prod_rev)
 next
   case True
   define m where "m = n - k"
   with True have n: "n = m + k"
     by arith
   from n have "fact n = ((\<Prod>i = 0..<m + k. of_nat (m + k - i) ):: 'a)"
-    by (simp add: fact_setprod_rev)
+    by (simp add: fact_prod_rev)
   also have "\<dots> = ((\<Prod>i\<in>{0..<k} \<union> {k..<m + k}. of_nat (m + k - i)) :: 'a)"
     by (simp add: ivl_disj_un)
   finally have "fact n = (fact m * (\<Prod>i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)"
-    using setprod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
-    by (simp add: fact_setprod_rev [of m] setprod.union_disjoint of_nat_diff)
+    using prod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
+    by (simp add: fact_prod_rev [of m] prod.union_disjoint of_nat_diff)
   then have "fact n / fact (n - k) = ((\<Prod>i = 0..<k. of_nat n - of_nat i) :: 'a)"
     by (simp add: n)
   with True have "fact k * of_nat (n gchoose k) = (fact k * (of_nat n gchoose k) :: 'a)"
@@ -800,10 +800,10 @@
   \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
 
 lemma gbinomial_1[simp]: "a gchoose 1 = a"
-  by (simp add: gbinomial_setprod_rev lessThan_Suc)
+  by (simp add: gbinomial_prod_rev lessThan_Suc)
 
 lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
-  by (simp add: gbinomial_setprod_rev lessThan_Suc)
+  by (simp add: gbinomial_prod_rev lessThan_Suc)
 
 lemma gbinomial_mult_1:
   fixes a :: "'a::field_char_0"
@@ -833,7 +833,7 @@
 next
   case (Suc h)
   have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
-    apply (rule setprod.reindex_cong [where l = Suc])
+    apply (rule prod.reindex_cong [where l = Suc])
       using Suc
       apply (auto simp add: image_Suc_atMost)
     done
@@ -865,7 +865,7 @@
     by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost)
   also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
     using eq0
-    by (simp add: Suc setprod.atLeast0_atMost_Suc_shift)
+    by (simp add: Suc prod.atLeast0_atMost_Suc_shift)
   also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
     by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost)
   finally show ?thesis
@@ -1003,7 +1003,7 @@
   Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}.\<close>
 lemma gbinomial_altdef_of_nat: "x gchoose k = (\<Prod>i = 0..<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
   for k :: nat and x :: "'a::field_char_0"
-  by (simp add: setprod_dividef gbinomial_setprod_rev fact_setprod_rev)
+  by (simp add: prod_dividef gbinomial_prod_rev fact_prod_rev)
 
 lemma gbinomial_ge_n_over_k_pow_k:
   fixes k :: nat
@@ -1014,10 +1014,10 @@
   have x: "0 \<le> x"
     using assms of_nat_0_le_iff order_trans by blast
   have "(x / of_nat k :: 'a) ^ k = (\<Prod>i = 0..<k. x / of_nat k :: 'a)"
-    by (simp add: setprod_constant)
+    by (simp add: prod_constant)
   also have "\<dots> \<le> x gchoose k" (* FIXME *)
     unfolding gbinomial_altdef_of_nat
-    apply (safe intro!: setprod_mono)
+    apply (safe intro!: prod_mono)
     apply simp_all
     prefer 2
     subgoal premises for i
@@ -1051,11 +1051,11 @@
 next
   case (Suc b)
   then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
-    by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+    by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
   also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
-    by (simp add: setprod.atLeast0_atMost_Suc_shift)
+    by (simp add: prod.atLeast0_atMost_Suc_shift)
   also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
-    by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+    by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
   finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
 qed
 
@@ -1066,11 +1066,11 @@
 next
   case (Suc b)
   then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)"
-    by (simp add: field_simps gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost)
+    by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
   also have "(\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
-    by (simp add: setprod.atLeast0_atMost_Suc_shift)
+    by (simp add: prod.atLeast0_atMost_Suc_shift)
   also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
-    by (simp_all add: gbinomial_setprod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
+    by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
   finally show ?thesis
     by (simp add: Suc)
 qed
@@ -1647,11 +1647,11 @@
   "fact n = (of_nat (fold_atLeastAtMost_nat (op *) 2 n 1) :: 'a::semiring_char_0)"
 proof -
   have "fact n = (of_nat (\<Prod>{1..n}) :: 'a)"
-    by (simp add: fact_setprod)
+    by (simp add: fact_prod)
   also have "\<Prod>{1..n} = \<Prod>{2..n}"
-    by (intro setprod.mono_neutral_right) auto
+    by (intro prod.mono_neutral_right) auto
   also have "\<dots> = fold_atLeastAtMost_nat (op *) 2 n 1"
-    by (simp add: setprod_atLeastAtMost_code)
+    by (simp add: prod_atLeastAtMost_code)
   finally show ?thesis .
 qed
 
@@ -1660,7 +1660,7 @@
     (if n = 0 then 1
      else fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
   by (cases n)
-    (simp_all add: pochhammer_setprod setprod_atLeastAtMost_code [symmetric]
+    (simp_all add: pochhammer_prod prod_atLeastAtMost_code [symmetric]
       atLeastLessThanSuc_atLeastAtMost)
 
 lemma gbinomial_code [code]:
@@ -1668,7 +1668,7 @@
     (if n = 0 then 1
      else fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
   by (cases n)
-    (simp_all add: gbinomial_setprod_rev setprod_atLeastAtMost_code [symmetric]
+    (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
       atLeastLessThanSuc_atLeastAtMost)
 
 (* FIXME *)
@@ -1685,9 +1685,9 @@
     assume "k \<le> n"
     then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
     then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
-      by (simp add: setprod.union_disjoint fact_altdef_nat)
+      by (simp add: prod.union_disjoint fact_altdef_nat)
   }
-  then show ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
+  then show ?thesis by (auto simp: binomial_altdef_nat mult_ac prod_atLeastAtMost_code)
 qed
 *)
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Complex.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -486,7 +486,7 @@
 lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
   by (simp add: complex_eq_iff)
 
-lemma cnj_setprod [simp]: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
+lemma cnj_prod [simp]: "cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
 lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -3972,7 +3972,7 @@
     qed
 
     have "\<And>k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
-    hence setprod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
+    hence prod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
       by auto
     have sum_move0: "\<And>k F. sum F {0..<Suc k} = F 0 + sum (\<lambda> k. F (Suc k)) {0..<k}"
       unfolding sum_shift_bounds_Suc_ivl[symmetric]
@@ -3994,7 +3994,7 @@
       also have "?X (Suc k) f n t * (xs!x - real_of_float c) * inverse (real k) + ?f 0 c =
                (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i c * (xs!x - c)^i) +
                inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - c)^Suc n" (is "_ = ?T")
-        unfolding funpow_Suc C_def[symmetric] sum_move0 setprod_head_Suc
+        unfolding funpow_Suc C_def[symmetric] sum_move0 prod_head_Suc
         by (auto simp add: algebra_simps)
           (simp only: mult.left_commute [of _ "inverse (real k)"] sum_distrib_left [symmetric])
       finally have "?T \<in> {l .. u}" .
@@ -4003,8 +4003,8 @@
   qed
 qed
 
-lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
-  by (simp add: fact_setprod atLeastLessThanSuc_atLeastAtMost)
+lemma prod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
+  by (simp add: fact_prod atLeastLessThanSuc_atLeastAtMost)
 
 lemma approx_tse:
   assumes "bounded_by xs vs"
@@ -4029,7 +4029,7 @@
            (\<Sum> j = 0..<n. inverse(fact j) * F j c * (xs!x - c)^j) +
              inverse ((fact n)) * F n t * (xs!x - c)^n
              \<in> {l .. u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
-    unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact
+    unfolding F_def atLeastAtMost_iff[symmetric] prod_fact
     by blast
 
   have bnd_xs: "xs ! x \<in> { lx .. ux }"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Deriv.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -351,7 +351,7 @@
 lemmas has_derivative_mult[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_mult]
 lemmas has_derivative_scaleR[simp, derivative_intros] = bounded_bilinear.FDERIV[OF bounded_bilinear_scaleR]
 
-lemma has_derivative_setprod[simp, derivative_intros]:
+lemma has_derivative_prod[simp, derivative_intros]:
   fixes f :: "'i \<Rightarrow> 'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
   shows "(\<And>i. i \<in> I \<Longrightarrow> (f i has_derivative f' i) (at x within s)) \<Longrightarrow>
     ((\<lambda>x. \<Prod>i\<in>I. f i x) has_derivative (\<lambda>y. \<Sum>i\<in>I. f' i y * (\<Prod>j\<in>I - {i}. f j x))) (at x within s)"
@@ -377,7 +377,7 @@
   fixes f :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_field"
   assumes f: "(f has_derivative f') (at x within s)"
   shows "((\<lambda>x. f x^n) has_derivative (\<lambda>y. of_nat n * f' y * f x^(n - 1))) (at x within s)"
-  using has_derivative_setprod[OF f, of "{..< n}"] by (simp add: setprod_constant ac_simps)
+  using has_derivative_prod[OF f, of "{..< n}"] by (simp add: prod_constant ac_simps)
 
 lemma has_derivative_inverse':
   fixes x :: "'a::real_normed_div_algebra"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/GCD.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -859,7 +859,7 @@
 lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   by (subst add_commute) simp
 
-lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
+lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
 
 lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
@@ -1373,7 +1373,7 @@
   also have "lcm a \<dots> = lcm a (\<Prod>A)"
     by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
   also from insert have "gcd a (\<Prod>A) = 1"
-    by (subst gcd.commute, intro setprod_coprime) auto
+    by (subst gcd.commute, intro prod_coprime) auto
   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
     by (simp add: lcm_coprime)
   finally show ?case .
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1051,34 +1051,34 @@
 context comm_monoid_mult
 begin
 
-sublocale setprod: comm_monoid_set times 1
-  defines setprod = setprod.F ..
+sublocale prod: comm_monoid_set times 1
+  defines prod = prod.F ..
 
-abbreviation Setprod ("\<Prod>_" [1000] 999)
-  where "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
+abbreviation Prod ("\<Prod>_" [1000] 999)
+  where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
 
 end
 
 syntax (ASCII)
-  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
+  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A"
+  "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
 
 text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
 
 syntax (ASCII)
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
+  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
 syntax
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
+  "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
 translations
-  "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
+  "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
 
 context comm_monoid_mult
 begin
 
-lemma setprod_dvd_setprod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
+lemma prod_dvd_prod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> prod f A dvd prod g A"
 proof (induct A rule: infinite_finite_induct)
   case infinite
   then show ?case by (auto intro: dvdI)
@@ -1087,18 +1087,18 @@
   then show ?case by (auto intro: dvdI)
 next
   case (insert a A)
-  then have "f a dvd g a" and "setprod f A dvd setprod g A"
+  then have "f a dvd g a" and "prod f A dvd prod g A"
     by simp_all
-  then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s"
+  then obtain r s where "g a = f a * r" and "prod g A = prod f A * s"
     by (auto elim!: dvdE)
-  then have "g a * setprod g A = f a * setprod f A * (r * s)"
+  then have "g a * prod g A = f a * prod f A * (r * s)"
     by (simp add: ac_simps)
   with insert.hyps show ?case
     by (auto intro: dvdI)
 qed
 
-lemma setprod_dvd_setprod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
-  by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
+lemma prod_dvd_prod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> prod f A dvd prod f B"
+  by (auto simp add: prod.subset_diff ac_simps intro: dvdI)
 
 end
 
@@ -1108,25 +1108,25 @@
 context comm_semiring_1
 begin
 
-lemma dvd_setprod_eqI [intro]:
+lemma dvd_prod_eqI [intro]:
   assumes "finite A" and "a \<in> A" and "b = f a"
-  shows "b dvd setprod f A"
+  shows "b dvd prod f A"
 proof -
-  from \<open>finite A\<close> have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
-    by (intro setprod.insert) auto
+  from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})"
+    by (intro prod.insert) auto
   also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A"
     by blast
-  finally have "setprod f A = f a * setprod f (A - {a})" .
+  finally have "prod f A = f a * prod f (A - {a})" .
   with \<open>b = f a\<close> show ?thesis
     by simp
 qed
 
-lemma dvd_setprodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd setprod f A"
+lemma dvd_prodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd prod f A"
   by auto
 
-lemma setprod_zero:
+lemma prod_zero:
   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
-  shows "setprod f A = 0"
+  shows "prod f A = 0"
   using assms
 proof (induct A)
   case empty
@@ -1134,32 +1134,32 @@
 next
   case (insert a A)
   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
-  then have "f a * setprod f A = 0" by rule (simp_all add: insert)
+  then have "f a * prod f A = 0" by rule (simp_all add: insert)
   with insert show ?case by simp
 qed
 
-lemma setprod_dvd_setprod_subset2:
+lemma prod_dvd_prod_subset2:
   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
-  shows "setprod f A dvd setprod g B"
+  shows "prod f A dvd prod g B"
 proof -
-  from assms have "setprod f A dvd setprod g A"
-    by (auto intro: setprod_dvd_setprod)
-  moreover from assms have "setprod g A dvd setprod g B"
-    by (auto intro: setprod_dvd_setprod_subset)
+  from assms have "prod f A dvd prod g A"
+    by (auto intro: prod_dvd_prod)
+  moreover from assms have "prod g A dvd prod g B"
+    by (auto intro: prod_dvd_prod_subset)
   ultimately show ?thesis by (rule dvd_trans)
 qed
 
 end
 
-lemma (in semidom) setprod_zero_iff [simp]:
+lemma (in semidom) prod_zero_iff [simp]:
   fixes f :: "'b \<Rightarrow> 'a"
   assumes "finite A"
-  shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+  shows "prod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   using assms by (induct A) (auto simp: no_zero_divisors)
 
-lemma (in semidom_divide) setprod_diff1:
+lemma (in semidom_divide) prod_diff1:
   assumes "finite A" and "f a \<noteq> 0"
-  shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
+  shows "prod f (A - {a}) = (if a \<in> A then prod f A div f a else prod f A)"
 proof (cases "a \<notin> A")
   case True
   then show ?thesis by simp
@@ -1196,73 +1196,73 @@
   for c :: "nat \<Rightarrow> 'a::field"
   using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
 
-lemma (in field) setprod_inversef:
-  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
+lemma (in field) prod_inversef:
+  "finite A \<Longrightarrow> prod (inverse \<circ> f) A = inverse (prod f A)"
   by (induct A rule: finite_induct) simp_all
 
-lemma (in field) setprod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
-  using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
+lemma (in field) prod_dividef: "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
+  using prod_inversef [of A g] by (simp add: divide_inverse prod.distrib)
 
-lemma setprod_Un:
+lemma prod_Un:
   fixes f :: "'b \<Rightarrow> 'a :: field"
   assumes "finite A" and "finite B"
     and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
-  shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
+  shows "prod f (A \<union> B) = prod f A * prod f B / prod f (A \<inter> B)"
 proof -
-  from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
-    by (simp add: setprod.union_inter [symmetric, of A B])
+  from assms have "prod f A * prod f B = prod f (A \<union> B) * prod f (A \<inter> B)"
+    by (simp add: prod.union_inter [symmetric, of A B])
   with assms show ?thesis
     by simp
 qed
 
-lemma (in linordered_semidom) setprod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
+lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma (in linordered_semidom) setprod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
+lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma (in linordered_semidom) setprod_mono:
-  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A"
-  by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono)
+lemma (in linordered_semidom) prod_mono:
+  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
+  by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
 
-lemma (in linordered_semidom) setprod_mono_strict:
+lemma (in linordered_semidom) prod_mono_strict:
   assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
-  shows "setprod f A < setprod g A"
+  shows "prod f A < prod g A"
   using assms
 proof (induct A rule: finite_induct)
   case empty
   then show ?case by simp
 next
   case insert
-  then show ?case by (force intro: mult_strict_mono' setprod_nonneg)
+  then show ?case by (force intro: mult_strict_mono' prod_nonneg)
 qed
 
-lemma (in linordered_field) abs_setprod: "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
+lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
 
-lemma setprod_eq_1_iff [simp]: "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
+lemma prod_eq_1_iff [simp]: "finite A \<Longrightarrow> prod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
   for f :: "'a \<Rightarrow> nat"
   by (induct A rule: finite_induct) simp_all
 
-lemma setprod_pos_nat_iff [simp]: "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
+lemma prod_pos_nat_iff [simp]: "finite A \<Longrightarrow> prod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
   for f :: "'a \<Rightarrow> nat"
-  using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
+  using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
 
-lemma setprod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
+lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
   for y :: "'a::comm_monoid_mult"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma setprod_power_distrib: "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
+lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
   for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
   by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
 
 lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
   by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
 
-lemma setprod_gen_delta:
+lemma prod_gen_delta:
   fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult"
   assumes fin: "finite S"
-  shows "setprod (\<lambda>k. if k = a then b k else c) S =
+  shows "prod (\<lambda>k. if k = a then b k else c) S =
     (if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)"
 proof -
   let ?f = "(\<lambda>k. if k=a then b k else c)"
@@ -1270,7 +1270,7 @@
   proof (cases "a \<in> S")
     case False
     then have "\<forall> k\<in> S. ?f k = c" by simp
-    with False show ?thesis by (simp add: setprod_constant)
+    with False show ?thesis by (simp add: prod_constant)
   next
     case True
     let ?A = "S - {a}"
@@ -1278,16 +1278,16 @@
     from True have eq: "S = ?A \<union> ?B" by blast
     have disjoint: "?A \<inter> ?B = {}" by simp
     from fin have fin': "finite ?A" "finite ?B" by auto
-    have f_A0: "setprod ?f ?A = setprod (\<lambda>i. c) ?A"
-      by (rule setprod.cong) auto
+    have f_A0: "prod ?f ?A = prod (\<lambda>i. c) ?A"
+      by (rule prod.cong) auto
     from fin True have card_A: "card ?A = card S - 1" by auto
-    have f_A1: "setprod ?f ?A = c ^ card ?A"
-      unfolding f_A0 by (rule setprod_constant)
-    have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
-      using setprod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
+    have f_A1: "prod ?f ?A = c ^ card ?A"
+      unfolding f_A0 by (rule prod_constant)
+    have "prod ?f ?A * prod ?f ?B = prod ?f S"
+      using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
       by simp
     with True card_A show ?thesis
-      by (simp add: f_A1 field_simps cong add: setprod.cong cong del: if_weak_cong)
+      by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong)
   qed
 qed
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Groups_List.thy
--- a/src/HOL/Groups_List.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Groups_List.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -340,15 +340,15 @@
   from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
 qed
 
-sublocale setprod: comm_monoid_list_set times 1
+sublocale prod: comm_monoid_list_set times 1
 rewrites
   "monoid_list.F times 1 = prod_list"
-  and "comm_monoid_set.F times 1 = setprod"
+  and "comm_monoid_set.F times 1 = prod"
 proof -
   show "comm_monoid_list_set times 1" ..
-  then interpret setprod: comm_monoid_list_set times 1 .
+  then interpret prod: comm_monoid_list_set times 1 .
   from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
-  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
+  from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
 qed
 
 end
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Int.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -866,7 +866,7 @@
 qed
 
 
-subsection \<open>@{term sum} and @{term setprod}\<close>
+subsection \<open>@{term sum} and @{term prod}\<close>
 
 lemma of_nat_sum [simp]: "of_nat (sum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   by (induct A rule: infinite_finite_induct) auto
@@ -874,14 +874,14 @@
 lemma of_int_sum [simp]: "of_int (sum f A) = (\<Sum>x\<in>A. of_int(f x))"
   by (induct A rule: infinite_finite_induct) auto
 
-lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+lemma of_nat_prod [simp]: "of_nat (prod f A) = (\<Prod>x\<in>A. of_nat(f x))"
   by (induct A rule: infinite_finite_induct) auto
 
-lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
   by (induct A rule: infinite_finite_induct) auto
 
 lemmas int_sum = of_nat_sum [where 'a=int]
-lemmas int_setprod = of_nat_setprod [where 'a=int]
+lemmas int_prod = of_nat_prod [where 'a=int]
 
 
 text \<open>Legacy theorems\<close>
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -550,12 +550,12 @@
 lemma top_power_ennreal: "top ^ n = (if n = 0 then 1 else top :: ennreal)"
   by (induction n) (simp_all add: ennreal_mult_eq_top_iff)
 
-lemma ennreal_setprod_eq_0[simp]:
+lemma ennreal_prod_eq_0[simp]:
   fixes f :: "'a \<Rightarrow> ennreal"
-  shows "(setprod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
+  shows "(prod f A = 0) = (finite A \<and> (\<exists>i\<in>A. f i = 0))"
   by (induction A rule: infinite_finite_induct) auto
 
-lemma ennreal_setprod_eq_top:
+lemma ennreal_prod_eq_top:
   fixes f :: "'a \<Rightarrow> ennreal"
   shows "(\<Prod>i\<in>I. f i) = top \<longleftrightarrow> (finite I \<and> ((\<forall>i\<in>I. f i \<noteq> 0) \<and> (\<exists>i\<in>I. f i = top)))"
   by (induction I rule: infinite_finite_induct) (auto simp: ennreal_mult_eq_top_iff)
@@ -1047,9 +1047,9 @@
 lemma ennreal_divide_numeral: "0 \<le> x \<Longrightarrow> ennreal x / numeral b = ennreal (x / numeral b)"
   by (subst divide_ennreal[symmetric]) auto
 
-lemma setprod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (setprod f A)"
+lemma prod_ennreal: "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> (\<Prod>i\<in>A. ennreal (f i)) = ennreal (prod f A)"
   by (induction A rule: infinite_finite_induct)
-     (auto simp: ennreal_mult setprod_nonneg)
+     (auto simp: ennreal_mult prod_nonneg)
 
 lemma mult_right_ennreal_cancel: "a * ennreal c = b * ennreal c \<longleftrightarrow> (a = b \<or> c \<le> 0)"
   apply (cases "0 \<le> c")
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1180,7 +1180,7 @@
   shows "y \<le> x"
   by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
 
-lemma setprod_ereal_0:
+lemma prod_ereal_0:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
 proof (cases "finite A")
@@ -1191,7 +1191,7 @@
   then show ?thesis by auto
 qed
 
-lemma setprod_ereal_pos:
+lemma prod_ereal_pos:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   shows "0 \<le> (\<Prod>i\<in>I. f i)"
@@ -1204,7 +1204,7 @@
   then show ?thesis by simp
 qed
 
-lemma setprod_PInf:
+lemma prod_PInf:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
@@ -1213,15 +1213,15 @@
   from this assms show ?thesis
   proof (induct I)
     case (insert i I)
-    then have pos: "0 \<le> f i" "0 \<le> setprod f I"
-      by (auto intro!: setprod_ereal_pos)
-    from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>"
+    then have pos: "0 \<le> f i" "0 \<le> prod f I"
+      by (auto intro!: prod_ereal_pos)
+    from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> prod f I * f i = \<infinity>"
       by auto
-    also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
-      using setprod_ereal_pos[of I f] pos
-      by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
+    also have "\<dots> \<longleftrightarrow> (prod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> prod f I \<noteq> 0"
+      using prod_ereal_pos[of I f] pos
+      by (cases rule: ereal2_cases[of "f i" "prod f I"]) auto
     also have "\<dots> \<longleftrightarrow> finite (insert i I) \<and> (\<exists>j\<in>insert i I. f j = \<infinity>) \<and> (\<forall>j\<in>insert i I. f j \<noteq> 0)"
-      using insert by (auto simp: setprod_ereal_0)
+      using insert by (auto simp: prod_ereal_0)
     finally show ?case .
   qed simp
 next
@@ -1229,7 +1229,7 @@
   then show ?thesis by simp
 qed
 
-lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
+lemma prod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (prod f A)"
 proof (cases "finite A")
   case True
   then show ?thesis
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -2278,11 +2278,11 @@
 qed
 
 text \<open>The general form.\<close>
-lemma fps_setprod_nth:
+lemma fps_prod_nth:
   fixes m :: nat
     and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
-  shows "(setprod a {0 .. m}) $ n =
-    sum (\<lambda>v. setprod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
+  shows "(prod a {0 .. m}) $ n =
+    sum (\<lambda>v. prod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
   (is "?P m n")
 proof (induct m arbitrary: n rule: nat_less_induct)
   fix m n assume H: "\<forall>m' < m. \<forall>n. ?P m' n"
@@ -2301,8 +2301,8 @@
       using Suc by (simp add: set_eq_iff) presburger
     have f0: "finite {0 .. k}" "finite {m}" by auto
     have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto
-    have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n"
-      unfolding setprod.union_disjoint[OF f0 d0, unfolded u0] by simp
+    have "(prod a {0 .. m}) $ n = (prod a {0 .. k} * a m) $ n"
+      unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp
     also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). \<Prod>j\<in>{0..k}. a j $ v ! j) * a m $ (n - i))"
       unfolding fps_mult_nth H[rule_format, OF km] ..
     also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)"
@@ -2325,7 +2325,7 @@
       apply (rule_tac l = "\<lambda>xs. xs @ [n - x]" in sum.reindex_cong)
       apply (simp add: inj_on_def)
       apply auto
-      unfolding setprod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc]
+      unfolding prod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc]
       apply (clarsimp simp add: natpermute_def nth_append)
       done
     finally show ?thesis .
@@ -2336,18 +2336,18 @@
 lemma fps_power_nth_Suc:
   fixes m :: nat
     and a :: "'a::comm_ring_1 fps"
-  shows "(a ^ Suc m)$n = sum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
+  shows "(a ^ Suc m)$n = sum (\<lambda>v. prod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
 proof -
-  have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}"
-    by (simp add: setprod_constant)
-  show ?thesis unfolding th0 fps_setprod_nth ..
+  have th0: "a^Suc m = prod (\<lambda>i. a) {0..m}"
+    by (simp add: prod_constant)
+  show ?thesis unfolding th0 fps_prod_nth ..
 qed
 
 lemma fps_power_nth:
   fixes m :: nat
     and a :: "'a::comm_ring_1 fps"
   shows "(a ^m)$n =
-    (if m=0 then 1$n else sum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
+    (if m=0 then 1$n else sum (\<lambda>v. prod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
   by (cases m) (simp_all add: fps_power_nth_Suc del: power_Suc)
 
 lemma fps_nth_power_0:
@@ -2360,10 +2360,10 @@
 next
   case (Suc n)
   then have c: "m = card {0..n}" by simp
-  have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
+  have "(a ^m)$0 = prod (\<lambda>i. a$0) {0..n}"
     by (simp add: Suc fps_power_nth del: replicate.simps power_Suc)
   also have "\<dots> = (a$0) ^ m"
-   unfolding c by (rule setprod_constant)
+   unfolding c by (rule prod_constant)
  finally show ?thesis .
 qed
 
@@ -2433,10 +2433,10 @@
       
     from j have "{0..m} = insert j ({0..m} - {j})" by auto
     also from j have "(\<Prod>i\<in>\<dots>. f $ (v ! i)) = f $ k * (\<Prod>i\<in>{0..m} - {j}. f $ (v ! i))"
-      by (subst setprod.insert) auto
+      by (subst prod.insert) auto
     also have "(\<Prod>i\<in>{0..m} - {j}. f $ (v ! i)) = (\<Prod>i\<in>{0..m} - {j}. f $ 0)"
-      by (intro setprod.cong) (simp_all add: zero)
-    also from j have "\<dots> = (f $ 0) ^ m" by (subst setprod_constant) simp_all
+      by (intro prod.cong) (simp_all add: zero)
+    also from j have "\<dots> = (f $ 0) ^ m" by (subst prod_constant) simp_all
     finally have "(\<Prod>j = 0..m. f $ (v ! j)) = f $ k * (f $ 0) ^ m" .
   } note A = this
   
@@ -2472,7 +2472,7 @@
         using that elem_le_sum_list_nat[of i v] unfolding natpermute_def
         by (auto simp: set_conv_nth dest!: spec[of _ i])
       hence "?h f = ?h g"
-        by (intro sum.cong refl setprod.cong less lessI) (auto simp: natpermute_def)
+        by (intro sum.cong refl prod.cong less lessI) (auto simp: natpermute_def)
       finally have "f $ k * (of_nat (Suc m) * (f $ 0) ^ m) = g $ k * (of_nat (Suc m) * (f $ 0) ^ m)"
         by simp
       with assms show "f $ k = g $ k" 
@@ -2567,7 +2567,7 @@
 
 subsection \<open>Radicals\<close>
 
-declare setprod.cong [fundef_cong]
+declare prod.cong [fundef_cong]
 
 function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a::field fps \<Rightarrow> nat \<Rightarrow> 'a"
 where
@@ -2575,7 +2575,7 @@
 | "radical r 0 a (Suc n) = 0"
 | "radical r (Suc k) a 0 = r (Suc k) (a$0)"
 | "radical r (Suc k) a (Suc n) =
-    (a$ Suc n - sum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
+    (a$ Suc n - sum (\<lambda>xs. prod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
       {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) /
     (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
   by pat_completeness auto
@@ -2641,14 +2641,14 @@
   have eq1: "fps_radical r k a ^ k $ 0 = (\<Prod>j\<in>{0..h}. fps_radical r k a $ (replicate k 0) ! j)"
     unfolding fps_power_nth Suc by simp
   also have "\<dots> = (\<Prod>j\<in>{0..h}. r k (a$0))"
-    apply (rule setprod.cong)
+    apply (rule prod.cong)
     apply simp
     using Suc
     apply (subgoal_tac "replicate k 0 ! x = 0")
     apply (auto intro: nth_replicate simp del: replicate.simps)
     done
   also have "\<dots> = a$0"
-    using r Suc by (simp add: setprod_constant)
+    using r Suc by (simp add: prod_constant)
   finally show ?thesis
     using Suc by simp
 qed
@@ -2693,12 +2693,12 @@
             unfolding natpermute_contain_maximal by auto
           have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) =
               (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
-            apply (rule setprod.cong, simp)
+            apply (rule prod.cong, simp)
             using i r0
             apply (simp del: replicate.simps)
             done
           also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
-            using i r0 by (simp add: setprod_gen_delta)
+            using i r0 by (simp add: prod_gen_delta)
           finally show ?ths .
         qed rule
         then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
@@ -2720,7 +2720,7 @@
       by simp
     then show ?thesis
       unfolding fps_power_nth_Suc
-      by (simp add: setprod_constant del: replicate.simps)
+      by (simp add: prod_constant del: replicate.simps)
   qed
 qed
 
@@ -2757,10 +2757,10 @@
           from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
             unfolding natpermute_contain_maximal by auto
           have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
-            apply (rule setprod.cong, simp)
+            apply (rule prod.cong, simp)
             using i r0 by (simp del: replicate.simps)
           also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
-            unfolding setprod_gen_delta[OF fK] using i r0 by simp
+            unfolding prod_gen_delta[OF fK] using i r0 by simp
           finally show ?ths .
         qed
         then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
@@ -2828,18 +2828,18 @@
             unfolding Suc_eq_plus1 natpermute_contain_maximal
             by (auto simp del: replicate.simps)
           have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
-            apply (rule setprod.cong, simp)
+            apply (rule prod.cong, simp)
             using i a0
             apply (simp del: replicate.simps)
             done
           also have "\<dots> = a $ n * (?r $ 0)^k"
-            using i by (simp add: setprod_gen_delta)
+            using i by (simp add: prod_gen_delta)
           finally show ?ths .
         qed rule
         then have th0: "sum ?g ?Pnkn = of_nat (k+1) * a $ n * (?r $ 0)^k"
           by (simp add: natpermute_max_card[OF nz, simplified])
         have th1: "sum ?g ?Pnknn = sum ?f ?Pnknn"
-        proof (rule sum.cong, rule refl, rule setprod.cong, simp)
+        proof (rule sum.cong, rule refl, rule prod.cong, simp)
           fix xs i
           assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}"
           have False if c: "n \<le> xs ! i"
@@ -3380,9 +3380,9 @@
   apply (simp add: fps_compose_nth fps_mult_nth sum_distrib_right)
   done
 
-lemma fps_compose_setprod_distrib:
+lemma fps_compose_prod_distrib:
   assumes c0: "c$0 = (0::'a::idom)"
-  shows "setprod a S oo c = setprod (\<lambda>k. a k oo c) S"
+  shows "prod a S oo c = prod (\<lambda>k. a k oo c) S"
   apply (cases "finite S")
   apply simp_all
   apply (induct S rule: finite_induct)
@@ -3413,10 +3413,10 @@
   then show ?thesis by simp
 next
   case (Suc m)
-  have th0: "a^n = setprod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = setprod (\<lambda>k. a oo c) {0..m}"
-    by (simp_all add: setprod_constant Suc)
+  have th0: "a^n = prod (\<lambda>k. a) {0..m}" "(a oo c) ^ n = prod (\<lambda>k. a oo c) {0..m}"
+    by (simp_all add: prod_constant Suc)
   then show ?thesis
-    by (simp add: fps_compose_setprod_distrib[OF c0])
+    by (simp add: fps_compose_prod_distrib[OF c0])
 qed
 
 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
@@ -4155,8 +4155,8 @@
         case False
         with kn have kn': "k < n"
           by simp
-        have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
-          by (simp_all add: setprod_constant m h)
+        have m1nk: "?m1 n = prod (\<lambda>i. - 1) {..m}" "?m1 k = prod (\<lambda>i. - 1) {0..h}"
+          by (simp_all add: prod_constant m h)
         have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
           using bn0 kn
           unfolding pochhammer_eq_0_iff
@@ -4164,37 +4164,37 @@
           apply (erule_tac x= "n - ka - 1" in allE)
           apply (auto simp add: algebra_simps of_nat_diff)
           done
-        have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
-          setprod of_nat {Suc (m - h) .. Suc m}"
+        have eq1: "prod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
+          prod of_nat {Suc (m - h) .. Suc m}"
           using kn' h m
-          by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
+          by (intro prod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
              (auto simp: of_nat_diff)
         have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
           apply (simp add: pochhammer_minus field_simps)
           using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n])
-          apply (simp add: pochhammer_setprod)
-          using setprod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
+          apply (simp add: pochhammer_prod)
+          using prod.atLeast_lessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
           apply (auto simp add: of_nat_diff field_simps)
           done
-        have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
+        have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}"
           apply (simp add: pochhammer_minus field_simps m)
-          apply (auto simp add: pochhammer_setprod_rev of_nat_diff setprod.atLeast_Suc_atMost_Suc_shift)
+          apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift)
           done
-        have th21:"pochhammer (b - of_nat n + 1) k = setprod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
-          using kn apply (simp add: pochhammer_setprod_rev m h setprod.atLeast_Suc_atMost_Suc_shift)
-          using setprod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
+        have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
+          using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift)
+          using prod.atLeast_atMost_shift_0 [of "m - h" m, where ?'a = 'a]
           apply (auto simp add: of_nat_diff field_simps)
           done
         have "?m1 n * ?p b n =
-          setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
+          prod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
           using kn' m h unfolding th20 th21 apply simp
-          apply (subst setprod.union_disjoint [symmetric])
+          apply (subst prod.union_disjoint [symmetric])
           apply auto
-          apply (rule setprod.cong)
+          apply (rule prod.cong)
           apply auto
           done
         then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k =
-          setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
+          prod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
           using nz' by (simp add: field_simps)
         have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) =
           ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
@@ -4204,7 +4204,7 @@
           unfolding th1 th2
           using kn' m h
           apply (simp add: field_simps gbinomial_mult_fact)
-          apply (rule setprod.cong)
+          apply (rule prod.cong)
           apply auto
           done
         finally show ?thesis by simp
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -283,11 +283,11 @@
 
 sublocale Prod_any: comm_monoid_fun times 1
   defines Prod_any = Prod_any.G
-  rewrites "comm_monoid_set.F times 1 = setprod"
+  rewrites "comm_monoid_set.F times 1 = prod"
 proof -
   show "comm_monoid_fun times 1" ..
   then interpret Prod_any: comm_monoid_fun times 1 .
-  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
+  from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
 qed
 
 end
@@ -308,7 +308,7 @@
   from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
   with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
   with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
-    by (simp add: Prod_any.expand_set setprod_zero)
+    by (simp add: Prod_any.expand_set prod_zero)
 qed
 
 lemma Prod_any_not_zero:
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -2269,13 +2269,13 @@
   "prod_mset (replicate_mset n a) = a ^ n"
   by (induct n) simp_all
 
-lemma setprod_unfold_prod_mset:
-  "setprod f A = prod_mset (image_mset f (mset_set A))"
+lemma prod_unfold_prod_mset:
+  "prod f A = prod_mset (image_mset f (mset_set A))"
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma prod_mset_multiplicity:
-  "prod_mset M = setprod (\<lambda>x. x ^ count M x) (set_mset M)"
-  by (simp add: fold_mset_def setprod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
+  "prod_mset M = prod (\<lambda>x. x ^ count M x) (set_mset M)"
+  by (simp add: fold_mset_def prod.eq_fold prod_mset.eq_fold funpow_times_power comp_def)
 
 lemma prod_mset_delta: "prod_mset (image_mset (\<lambda>x. if x = y then c else 1) A) = c ^ count A y"
   by (induction A) simp_all
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Multiset_Permutations.thy
--- a/src/HOL/Library/Multiset_Permutations.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -161,24 +161,24 @@
 context
 begin
 
-private lemma multiset_setprod_fact_insert:
+private lemma multiset_prod_fact_insert:
   "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
      (count A x + 1) * (\<Prod>y\<in>set_mset A. fact (count A y))"
 proof -
   have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
           (\<Prod>y\<in>set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))"
-    by (intro setprod.cong) simp_all
+    by (intro prod.cong) simp_all
   also have "\<dots> = (count A x + 1) * (\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y))"
-    by (simp add: setprod.distrib setprod.delta)
+    by (simp add: prod.distrib prod.delta)
   also have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y)) = (\<Prod>y\<in>set_mset A. fact (count A y))"
-    by (intro setprod.mono_neutral_right) (auto simp: not_in_iff)
+    by (intro prod.mono_neutral_right) (auto simp: not_in_iff)
   finally show ?thesis .
 qed
 
-private lemma multiset_setprod_fact_remove:
+private lemma multiset_prod_fact_remove:
   "x \<in># A \<Longrightarrow> (\<Prod>y\<in>set_mset A. fact (count A y)) =
                    count A x * (\<Prod>y\<in>set_mset (A-{#x#}). fact (count (A-{#x#}) y))"
-  using multiset_setprod_fact_insert[of "A - {#x#}" x] by simp
+  using multiset_prod_fact_insert[of "A - {#x#}" x] by simp
 
 lemma card_permutations_of_multiset_aux:
   "card (permutations_of_multiset A) * (\<Prod>x\<in>set_mset A. fact (count A x)) = fact (size A)"
@@ -199,7 +199,7 @@
     have "card (permutations_of_multiset (A - {#x#})) * (\<Prod>y\<in>set_mset A. fact (count A y)) = 
             count A x * (card (permutations_of_multiset (A - {#x#})) * 
               (\<Prod>y\<in>set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _")
-      by (subst multiset_setprod_fact_remove[OF x]) simp_all
+      by (subst multiset_prod_fact_remove[OF x]) simp_all
     also note remove.IH[OF x]
     also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset)
     finally show "?lhs = count A x * fact (size A - 1)" .
@@ -223,7 +223,7 @@
 proof -
   note card_permutations_of_multiset_aux[of "A + {#x#}"]
   also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp
-  also note multiset_setprod_fact_insert[of A x]
+  also note multiset_prod_fact_insert[of A x]
   also note card_permutations_of_multiset_aux[of A, symmetric]
   finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) *
                     (\<Prod>y\<in>set_mset A. fact (count A y)) =
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1054,13 +1054,13 @@
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n) simp_all
 
-lemma poly_setprod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
+lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)"
   by (induct A rule: infinite_finite_induct) simp_all
 
-lemma degree_setprod_sum_le: "finite S \<Longrightarrow> degree (setprod f S) \<le> sum (degree o f) S"
+lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree o f) S"
 proof (induct S rule: finite_induct)
   case (insert a S)
-  show ?case unfolding setprod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
+  show ?case unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
     by (rule le_trans[OF degree_mult_le], insert insert, auto)
 qed simp
 
@@ -2856,7 +2856,7 @@
   by (cases "finite A", induction rule: finite_induct)
      (simp_all add: pcompose_1 pcompose_add)
 
-lemma pcompose_setprod: "pcompose (setprod f A) p = setprod (\<lambda>i. pcompose (f i) p) A"
+lemma pcompose_prod: "pcompose (prod f A) p = prod (\<lambda>i. pcompose (f i) p) A"
   by (cases "finite A", induction rule: finite_induct)
      (simp_all add: pcompose_1 pcompose_mult)
 
@@ -3209,9 +3209,9 @@
        reflect_poly p ^ n"
   by (induction n) (simp_all add: reflect_poly_mult)
 
-lemma reflect_poly_setprod:
-  "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) = 
-     setprod (\<lambda>x. reflect_poly (f x)) A"
+lemma reflect_poly_prod:
+  "reflect_poly (prod (f :: _ \<Rightarrow> _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) = 
+     prod (\<lambda>x. reflect_poly (f x)) A"
   by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
 
 lemma reflect_poly_prod_list:
@@ -3225,7 +3225,7 @@
 
 lemmas reflect_poly_simps = 
   reflect_poly_0 reflect_poly_1 reflect_poly_const reflect_poly_smult reflect_poly_mult
-  reflect_poly_power reflect_poly_setprod reflect_poly_prod_list
+  reflect_poly_power reflect_poly_prod reflect_poly_prod_list
 
 
 subsection \<open>Derivatives of univariate polynomials\<close>
@@ -3395,11 +3395,11 @@
 apply (simp add: algebra_simps)
 done
 
-lemma pderiv_setprod: "pderiv (setprod f (as)) = 
-  (\<Sum>a \<in> as. setprod f (as - {a}) * pderiv (f a))"
+lemma pderiv_prod: "pderiv (prod f (as)) = 
+  (\<Sum>a \<in> as. prod f (as - {a}) * pderiv (f a))"
 proof (induct as rule: infinite_finite_induct)
   case (insert a as)
-  hence id: "setprod f (insert a as) = f a * setprod f as" 
+  hence id: "prod f (insert a as) = f a * prod f as" 
     "\<And> g. sum g (insert a as) = g a + sum g as"
     "insert a as - {a} = as"
     by auto
@@ -3407,9 +3407,9 @@
     fix b
     assume "b \<in> as"
     hence id2: "insert a as - {b} = insert a (as - {b})" using \<open>a \<notin> as\<close> by auto
-    have "setprod f (insert a as - {b}) = f a * setprod f (as - {b})"
+    have "prod f (insert a as - {b}) = f a * prod f (as - {b})"
       unfolding id2
-      by (subst setprod.insert, insert insert, auto)
+      by (subst prod.insert, insert insert, auto)
   } note id2 = this
   show ?case
     unfolding id pderiv_mult insert(3) sum_distrib_left
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/Polynomial_FPS.thy
--- a/src/HOL/Library/Polynomial_FPS.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/Polynomial_FPS.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -67,7 +67,7 @@
 lemma fps_of_poly_sum_list: "fps_of_poly (sum_list xs) = sum_list (map fps_of_poly xs)"
   by (induction xs) (simp_all add: fps_of_poly_add)
   
-lemma fps_of_poly_setprod: "fps_of_poly (setprod f A) = setprod (\<lambda>x. fps_of_poly (f x)) A"
+lemma fps_of_poly_prod: "fps_of_poly (prod f A) = prod (\<lambda>x. fps_of_poly (f x)) A"
   by (cases "finite A", induction rule: finite_induct) (simp_all add: fps_of_poly_mult)
   
 lemma fps_of_poly_prod_list: "fps_of_poly (prod_list xs) = prod_list (map fps_of_poly xs)"
@@ -144,7 +144,7 @@
 lemmas fps_of_poly_simps =
   fps_of_poly_0 fps_of_poly_1 fps_of_poly_numeral fps_of_poly_const fps_of_poly_X
   fps_of_poly_add fps_of_poly_diff fps_of_poly_uminus fps_of_poly_mult fps_of_poly_smult
-  fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_setprod fps_of_poly_prod_list
+  fps_of_poly_sum fps_of_poly_sum_list fps_of_poly_prod fps_of_poly_prod_list
   fps_of_poly_pCons fps_of_poly_pderiv fps_of_poly_power fps_of_poly_monom
   fps_of_poly_divide_numeral
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -88,7 +88,7 @@
   "sum = sum" ..
 
 lemma [code, code del]:
-  "setprod = setprod" ..
+  "prod = prod" ..
 
 lemma [code, code del]:
   "Product_Type.product = Product_Type.product"  ..
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Lifting_Set.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -286,7 +286,7 @@
 qed
 
 lemmas sum_parametric = sum.F_parametric
-lemmas setprod_parametric = setprod.F_parametric
+lemmas prod_parametric = prod.F_parametric
 
 lemma rel_set_UNION:
   assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Limits.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -833,20 +833,20 @@
   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. (f x)^n)"
   unfolding continuous_on_def by (auto intro: tendsto_power)
 
-lemma tendsto_setprod [tendsto_intros]:
+lemma tendsto_prod [tendsto_intros]:
   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   shows "(\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> L i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>S. f i x) \<longlongrightarrow> (\<Prod>i\<in>S. L i)) F"
   by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult)
 
-lemma continuous_setprod [continuous_intros]:
+lemma continuous_prod [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
-  unfolding continuous_def by (rule tendsto_setprod)
-
-lemma continuous_on_setprod [continuous_intros]:
+  unfolding continuous_def by (rule tendsto_prod)
+
+lemma continuous_on_prod [continuous_intros]:
   fixes f :: "'a \<Rightarrow> _ \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
-  unfolding continuous_on_def by (auto intro: tendsto_setprod)
+  unfolding continuous_on_def by (auto intro: tendsto_prod)
 
 lemma tendsto_of_real_iff:
   "((\<lambda>x. of_real (f x) :: 'a::real_normed_div_algebra) \<longlongrightarrow> of_real c) F \<longleftrightarrow> (f \<longlongrightarrow> c) F"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/List.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -4672,7 +4672,7 @@
   moreover
   have "Suc (card A - Suc k) = card A - k" using Suc.prems by simp
   then have "(card A - k) * \<Prod>{Suc (card A - k)..card A} = \<Prod>{Suc (card A - Suc k)..card A}"
-    by (subst setprod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
+    by (subst prod.insert[symmetric]) (simp add: atLeastAtMost_insertL)+
   ultimately show ?case
     by (simp add: card_image inj_Cons card_UN_disjoint Suc.hyps algebra_simps)
 qed
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Nat_Transfer.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -186,33 +186,33 @@
 ]
 
 
-text \<open>sum and setprod\<close>
+text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is nat *)
 lemma transfer_nat_int_sum_prod:
     "sum f A = sum (%x. f (nat x)) (int ` A)"
-    "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+    "prod f A = prod (%x. f (nat x)) (int ` A)"
   apply (subst sum.reindex)
   apply (unfold inj_on_def, auto)
-  apply (subst setprod.reindex)
+  apply (subst prod.reindex)
   apply (unfold inj_on_def o_def, auto)
 done
 
 (* this handles the case where the *range* of f is nat *)
 lemma transfer_nat_int_sum_prod2:
     "sum f A = nat(sum (%x. int (f x)) A)"
-    "setprod f A = nat(setprod (%x. int (f x)) A)"
+    "prod f A = nat(prod (%x. int (f x)) A)"
   apply (simp only: int_sum [symmetric] nat_int)
-  apply (simp only: int_setprod [symmetric] nat_int)
+  apply (simp only: int_prod [symmetric] nat_int)
   done
 
 lemma transfer_nat_int_sum_prod_closure:
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
-    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+    "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   unfolding nat_set_def
   apply (rule sum_nonneg)
   apply auto
-  apply (rule setprod_nonneg)
+  apply (rule prod_nonneg)
   apply auto
 done
 
@@ -223,28 +223,28 @@
 
 lemma transfer_nat_int_sum_prod_closure:
     "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
-    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+    "(!!x. x : A  ==> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   unfolding nat_set_def simp_implies_def
   apply (rule sum_nonneg)
   apply auto
-  apply (rule setprod_nonneg)
+  apply (rule prod_nonneg)
   apply auto
 done
 *)
 
 (* Making A = B in this lemma doesn't work. Why not?
-   Also, why aren't sum.cong and setprod.cong enough,
+   Also, why aren't sum.cong and prod.cong enough,
    with the previously mentioned rule turned on? *)
 
 lemma transfer_nat_int_sum_prod_cong:
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
       sum f A = sum g B"
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
-      setprod f A = setprod g B"
+      prod f A = prod g B"
   unfolding nat_set_def
   apply (subst sum.cong, assumption)
   apply auto [2]
-  apply (subst setprod.cong, assumption, auto)
+  apply (subst prod.cong, assumption, auto)
 done
 
 declare transfer_morphism_nat_int [transfer add
@@ -389,29 +389,29 @@
 ]
 
 
-text \<open>sum and setprod\<close>
+text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is int *)
 lemma transfer_int_nat_sum_prod:
     "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
-    "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+    "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
   apply (subst sum.reindex)
   apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
-  apply (subst setprod.reindex)
+  apply (subst prod.reindex)
   apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
-            cong: setprod.cong)
+            cong: prod.cong)
 done
 
 (* this handles the case where the *range* of f is int *)
 lemma transfer_int_nat_sum_prod2:
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
-      setprod f A = int(setprod (%x. nat (f x)) A)"
+      prod f A = int(prod (%x. nat (f x)) A)"
   unfolding is_nat_def
   by (subst int_sum) auto
 
 declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
-  cong: sum.cong setprod.cong]
+  cong: sum.cong prod.cong]
 
 end
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -193,7 +193,7 @@
   apply (auto intro: cong_add_int)
   done
 
-lemma cong_setprod_nat [rule_format]:
+lemma cong_prod_nat [rule_format]:
     "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
       [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
   apply (cases "finite A")
@@ -201,7 +201,7 @@
   apply (auto intro: cong_mult_nat)
   done
 
-lemma cong_setprod_int [rule_format]:
+lemma cong_prod_int [rule_format]:
     "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
       [(\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. g x)] (mod m)"
   apply (cases "finite A")
@@ -562,22 +562,22 @@
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   by (auto simp add: cong_altdef_int lcm_least) [1]
 
-lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_prod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
     (\<forall>i\<in>A. [(x::nat) = y] (mod m i)) \<longrightarrow>
       [x = y] (mod (\<Prod>i\<in>A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime)
+  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   done
 
-lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
+lemma cong_cong_prod_coprime_int [rule_format]: "finite A \<Longrightarrow>
     (\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
     (\<forall>i\<in>A. [(x::int) = y] (mod m i)) \<longrightarrow>
       [x = y] (mod (\<Prod>i\<in>A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis coprime_cong_mult_int gcd.commute setprod_coprime)
+  apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
   done
 
 lemma binary_chinese_remainder_aux_nat:
@@ -760,7 +760,7 @@
   fix i
   assume "i : A"
   with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
-    by (intro setprod_coprime, auto)
+    by (intro prod_coprime, auto)
   then have "EX x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by (elim cong_solve_coprime_nat)
   then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
@@ -769,7 +769,7 @@
     (mod (\<Prod>j \<in> A - {i}. m j))"
     by (subst mult.commute, rule cong_mult_self_nat)
   ultimately show "\<exists>a. [a = 1] (mod m i) \<and> [a = 0]
-      (mod setprod m (A - {i}))"
+      (mod prod m (A - {i}))"
     by blast
 qed
 
@@ -824,7 +824,7 @@
          [x = y] (mod (\<Prod>i\<in>A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime)
+  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
   done
 
 lemma chinese_remainder_unique_nat:
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -1294,12 +1294,12 @@
   using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
   by simp
 
-lemma prime_elem_multiplicity_setprod_distrib:
+lemma prime_elem_multiplicity_prod_distrib:
   assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
-  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
+  shows   "multiplicity p (prod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
 proof -
-  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
-    using assms by (subst setprod_unfold_prod_mset)
+  have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
+    using assms by (subst prod_unfold_prod_mset)
                    (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset 
                       multiset.map_comp o_def)
   also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
@@ -1352,7 +1352,7 @@
   "prime p \<Longrightarrow> prime_factors p = {p}"
   by (drule prime_factorization_prime) simp
 
-lemma setprod_prime_factors:
+lemma prod_prime_factors:
   assumes "x \<noteq> 0"
   shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
 proof -
@@ -1361,7 +1361,7 @@
   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
     by (subst prod_mset_multiplicity) simp_all
   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
-    by (intro setprod.cong) 
+    by (intro prod.cong) 
       (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
   finally show ?thesis ..
 qed
@@ -1751,12 +1751,12 @@
   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   also have "\<dots> = ?rhs1"
     by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
-          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
+          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
   finally show "gcd x y = ?rhs1" .
   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
   also have "\<dots> = ?rhs2"
     by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
-          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
+          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
   finally show "lcm x y = ?rhs2" .
 qed
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -209,8 +209,8 @@
   using p_prime A_ncong_p [OF assms]
   by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
 
-lemma A_prod_relprime: "gcd (setprod id A) p = 1"
-  by (metis id_def all_A_relprime setprod_coprime)
+lemma A_prod_relprime: "gcd (prod id A) p = 1"
+  by (metis id_def all_A_relprime prod_coprime)
 
 
 subsection \<open>Relationships Between Gauss Sets\<close>
@@ -242,15 +242,15 @@
 lemma C_card_eq_D_plus_E: "card C = card D + card E"
   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
 
-lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
-  by (metis C_eq D_E_disj finite_D finite_E inf_commute setprod.union_disjoint sup_commute)
+lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
+  by (metis C_eq D_E_disj finite_D finite_E inf_commute prod.union_disjoint sup_commute)
 
-lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
+lemma C_B_zcong_prod: "[prod id C = prod id B] (mod p)"
   apply (auto simp add: C_def)
   apply (insert finite_B SR_B_inj)
-  apply (drule setprod.reindex [of "\<lambda>x. x mod int p" B id])
+  apply (drule prod.reindex [of "\<lambda>x. x mod int p" B id])
   apply auto
-  apply (rule cong_setprod_int)
+  apply (rule cong_prod_int)
   apply (auto simp add: cong_int_def)
   done
 
@@ -295,25 +295,25 @@
   using finite_A F_Un_D_subset A_card_eq F_Un_D_card 
   by (auto simp add: card_seteq)
 
-lemma prod_D_F_eq_prod_A: "(setprod id D) * (setprod id F) = setprod id A"
-  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F setprod.union_disjoint)
+lemma prod_D_F_eq_prod_A: "(prod id D) * (prod id F) = prod id A"
+  by (metis F_D_disj F_Un_D_eq_A Int_commute Un_commute finite_D finite_F prod.union_disjoint)
 
-lemma prod_F_zcong: "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
+lemma prod_F_zcong: "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
 proof -
-  have FE: "setprod id F = setprod (op - p) E"
+  have FE: "prod id F = prod (op - p) E"
     apply (auto simp add: F_def)
     apply (insert finite_E inj_on_pminusx_E)
-    apply (drule setprod.reindex, auto)
+    apply (drule prod.reindex, auto)
     done
   then have "\<forall>x \<in> E. [(p-x) mod p = - x](mod p)"
     by (metis cong_int_def minus_mod_self1 mod_mod_trivial)
-  then have "[setprod ((\<lambda>x. x mod p) o (op - p)) E = setprod (uminus) E](mod p)"
+  then have "[prod ((\<lambda>x. x mod p) o (op - p)) E = prod (uminus) E](mod p)"
     using finite_E p_ge_2
-          cong_setprod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
+          cong_prod_int [of E "(\<lambda>x. x mod p) o (op - p)" uminus p]
     by auto
-  then have two: "[setprod id F = setprod (uminus) E](mod p)"
-    by (metis FE cong_cong_mod_int cong_refl_int cong_setprod_int minus_mod_self1)
-  have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
+  then have two: "[prod id F = prod (uminus) E](mod p)"
+    by (metis FE cong_cong_mod_int cong_refl_int cong_prod_int minus_mod_self1)
+  have "prod uminus E = (-1) ^ (card E) * (prod id E)"
     using finite_E by (induct set: finite) auto
   with two show ?thesis
     by simp
@@ -322,50 +322,50 @@
 
 subsection \<open>Gauss' Lemma\<close>
 
-lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
+lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
 by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
 
 theorem pre_gauss_lemma:
   "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
-  have "[setprod id A = setprod id F * setprod id D](mod p)"
-    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong)
-  then have "[setprod id A = ((-1)^(card E) * setprod id E) * setprod id D] (mod p)"
+  have "[prod id A = prod id F * prod id D](mod p)"
+    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
+  then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
     apply (rule cong_trans_int)
     apply (metis cong_scalar_int prod_F_zcong)
     done
-  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
+  then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
     by (metis C_prod_eq_D_times_E mult.commute mult.left_commute)
-  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
+  then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
     by (rule cong_trans_int) (metis C_B_zcong_prod cong_scalar2_int)
-  then have "[setprod id A = ((-1)^(card E) *
-    (setprod id ((\<lambda>x. x * a) ` A)))] (mod p)"
+  then have "[prod id A = ((-1)^(card E) *
+    (prod id ((\<lambda>x. x * a) ` A)))] (mod p)"
     by (simp add: B_def)
-  then have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. x * a) A))]
+  then have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. x * a) A))]
     (mod p)"
-    by (simp add: inj_on_xa_A setprod.reindex)
-  moreover have "setprod (\<lambda>x. x * a) A =
-    setprod (\<lambda>x. a) A * setprod id A"
+    by (simp add: inj_on_xa_A prod.reindex)
+  moreover have "prod (\<lambda>x. x * a) A =
+    prod (\<lambda>x. a) A * prod id A"
     using finite_A by (induct set: finite) auto
-  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (\<lambda>x. a) A *
-    setprod id A))] (mod p)"
+  ultimately have "[prod id A = ((-1)^(card E) * (prod (\<lambda>x. a) A *
+    prod id A))] (mod p)"
     by simp
-  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
-      setprod id A)](mod p)"
+  then have "[prod id A = ((-1)^(card E) * a^(card A) *
+      prod id A)](mod p)"
     apply (rule cong_trans_int)
-    apply (simp add: cong_scalar2_int cong_scalar_int finite_A setprod_constant mult.assoc)
+    apply (simp add: cong_scalar2_int cong_scalar_int finite_A prod_constant mult.assoc)
     done
-  then have a: "[setprod id A * (-1)^(card E) =
-      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
+  then have a: "[prod id A * (-1)^(card E) =
+      ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
     by (rule cong_scalar_int)
-  then have "[setprod id A * (-1)^(card E) = setprod id A *
+  then have "[prod id A * (-1)^(card E) = prod id A *
       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
     apply (rule cong_trans_int)
     apply (simp add: a mult.commute mult.left_commute)
     done
-  then have "[setprod id A * (-1)^(card E) = setprod id A * a^(card A)](mod p)"
+  then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
     apply (rule cong_trans_int)
-    apply (simp add: aux cong del: setprod.strong_cong)
+    apply (simp add: aux cong del: prod.strong_cong)
     done
   with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (metis cong_mult_lcancel_int)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -485,11 +485,11 @@
 
 lemma prime_factorization_nat:
     "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
-  by (simp add: setprod_prime_factors)
+  by (simp add: prod_prime_factors)
 
 lemma prime_factorization_int:
     "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
-  by (simp add: setprod_prime_factors)
+  by (simp add: prod_prime_factors)
 
 lemma prime_factorization_unique_nat:
   fixes f :: "nat \<Rightarrow> _"
@@ -524,13 +524,13 @@
   by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
 
 (* TODO Move *)
-lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
+lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A"
   by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
 
 lemma primes_characterization'_int [rule_format]:
   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
       prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
-  by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
+  by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
 
 lemma multiplicity_characterization_nat:
   "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
@@ -545,7 +545,7 @@
 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
   by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric]) 
-     (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
+     (auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
 
 lemma multiplicity_characterization'_int [rule_format]:
   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
@@ -583,11 +583,11 @@
     unfolding set_mset_def count_A by (auto simp: g_def)
   with assms have prime: "prime x" if "x \<in># A" for x using that by auto
   from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
-    by (intro setprod.cong) (auto simp: g_def)
+    by (intro prod.cong) (auto simp: g_def)
   also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
-    by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
+    by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
   also have "\<dots> = prod_mset A"
-    by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: setprod.cong)
+    by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
   also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
     by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
   also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
@@ -601,10 +601,10 @@
   shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
   using assms by (induct A) (auto simp add: prime_factorization_mult)
 
-lemma prime_factors_setprod:
+lemma prime_factors_prod:
   assumes "finite A" and "0 \<notin> f ` A"
-  shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
-  using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset)
+  shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
+  using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
 
 lemma prime_factors_fact:
   "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
@@ -621,7 +621,7 @@
       by (auto intro: order_trans)
   } note * = this
   show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
-    by (auto simp add: fact_setprod prime_factors_setprod Suc_le_eq dest!: prime_prime_factors intro: *)
+    by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
 qed
 
 lemma prime_dvd_fact_iff:
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -428,10 +428,10 @@
     apply auto
     done
   also have "\<dots> = fact (p - 1) mod p"
-    apply (simp add: fact_setprod)
+    apply (simp add: fact_prod)
     apply (insert assms)
     apply (subst res_prime_units_eq)
-    apply (simp add: int_setprod zmod_int setprod_int_eq)
+    apply (simp add: int_prod zmod_int prod_int_eq)
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .
   then show ?thesis
@@ -445,7 +445,7 @@
 proof (cases "p = 2")
   case True
   then show ?thesis
-    by (simp add: cong_int_def fact_setprod)
+    by (simp add: cong_int_def fact_prod)
 next
   case False
   then show ?thesis
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Euler.thy
--- a/src/HOL/Old_Number_Theory/Euler.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -133,7 +133,7 @@
   then show ?thesis by auto
 qed
 
-lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
+lemma SetS_prod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
                               ~(QuadRes p a); x \<in> (SetS a p) |] ==> 
                           [\<Prod>x = a] (mod p)"
   apply (auto simp add: SetS_def MultInvPair_def)
@@ -174,21 +174,21 @@
   apply (frule d22set_g_1, auto)
   done
 
-lemma Union_SetS_setprod_prop1:
+lemma Union_SetS_prod_prop1:
   assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
     "~(QuadRes p a)"
   shows "[\<Prod>(\<Union>(SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
 proof -
-  from assms have "[\<Prod>(\<Union>(SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
+  from assms have "[\<Prod>(\<Union>(SetS a p)) = prod (prod (%x. x)) (SetS a p)] (mod p)"
     by (auto simp add: SetS_finite SetS_elems_finite
-      MultInvPair_prop1c setprod.Union_disjoint)
-  also have "[setprod (setprod (%x. x)) (SetS a p) = 
-      setprod (%x. a) (SetS a p)] (mod p)"
-    by (rule setprod_same_function_zcong)
-      (auto simp add: assms SetS_setprod_prop SetS_finite)
-  also (zcong_trans) have "[setprod (%x. a) (SetS a p) = 
+      MultInvPair_prop1c prod.Union_disjoint)
+  also have "[prod (prod (%x. x)) (SetS a p) = 
+      prod (%x. a) (SetS a p)] (mod p)"
+    by (rule prod_same_function_zcong)
+      (auto simp add: assms SetS_prod_prop SetS_finite)
+  also (zcong_trans) have "[prod (%x. a) (SetS a p) = 
       a^(card (SetS a p))] (mod p)"
-    by (auto simp add: assms SetS_finite setprod_constant)
+    by (auto simp add: assms SetS_finite prod_constant)
   finally (zcong_trans) show ?thesis
     apply (rule zcong_trans)
     apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
@@ -197,7 +197,7 @@
     done
 qed
 
-lemma Union_SetS_setprod_prop2:
+lemma Union_SetS_prod_prop2:
   assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
   shows "\<Prod>(\<Union>(SetS a p)) = zfact (p - 1)"
 proof -
@@ -219,8 +219,8 @@
 
 lemma zfact_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
                    [zfact (p - 1) = a ^ nat ((p - 1) div 2)] (mod p)"
-  apply (frule Union_SetS_setprod_prop1) 
-  apply (auto simp add: Union_SetS_setprod_prop2)
+  apply (frule Union_SetS_prod_prop1) 
+  apply (auto simp add: Union_SetS_prod_prop2)
   done
 
 text \<open>\medskip Prove the first part of Euler's Criterion:\<close>
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/EulerFermat.thy
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -252,7 +252,7 @@
    apply (simplesubst BnorRset.simps)  \<comment>\<open>multiple redexes\<close>
    apply (unfold Let_def, auto)
   apply (simp add: Bnor_fin Bnor_mem_zle_swap)
-  apply (subst setprod.insert)
+  apply (subst prod.insert)
     apply (rule_tac [2] Bnor_prod_power_aux)
      apply (unfold inj_on_def)
      apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -26,9 +26,9 @@
   assume "infinite S" thus ?thesis by simp
 qed
 
-lemma setprod_same_function_zcong:
+lemma prod_same_function_zcong:
   assumes a: "\<forall>x \<in> S. [f x = g x](mod m)"
-  shows "[setprod f S = setprod g S] (mod m)"
+  shows "[prod f S = prod g S] (mod m)"
 proof cases
   assume "finite S"
   thus ?thesis using a by induct (simp_all add: zcong_zmult)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -263,7 +263,7 @@
 lemma all_A_relprime: "\<forall>x \<in> A. zgcd x p = 1"
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
 
-lemma A_prod_relprime: "zgcd (setprod id A) p = 1"
+lemma A_prod_relprime: "zgcd (prod id A) p = 1"
 by(rule all_relprime_prod_relprime[OF finite_A all_A_relprime])
 
 
@@ -292,18 +292,18 @@
 lemma C_card_eq_D_plus_E: "card C = card D + card E"
   by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
 
-lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
+lemma C_prod_eq_D_times_E: "prod id E * prod id D = prod id C"
   apply (insert D_E_disj finite_D finite_E C_eq)
-  apply (frule setprod.union_disjoint [of D E id])
+  apply (frule prod.union_disjoint [of D E id])
   apply auto
   done
 
-lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
+lemma C_B_zcong_prod: "[prod id C = prod id B] (mod p)"
   apply (auto simp add: C_def)
   apply (insert finite_B SR_B_inj)
-  apply (frule setprod.reindex [of "StandardRes p" B id])
+  apply (frule prod.reindex [of "StandardRes p" B id])
   apply auto
-  apply (rule setprod_same_function_zcong)
+  apply (rule prod_same_function_zcong)
   apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   done
 
@@ -372,25 +372,25 @@
   using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
 
 lemma prod_D_F_eq_prod_A:
-    "(setprod id D) * (setprod id F) = setprod id A"
+    "(prod id D) * (prod id F) = prod id A"
   apply (insert F_D_disj finite_D finite_F)
-  apply (frule setprod.union_disjoint [of F D id])
+  apply (frule prod.union_disjoint [of F D id])
   apply (auto simp add: F_Un_D_eq_A)
   done
 
 lemma prod_F_zcong:
-  "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
+  "[prod id F = ((-1) ^ (card E)) * (prod id E)] (mod p)"
 proof -
-  have "setprod id F = setprod id (op - p ` E)"
+  have "prod id F = prod id (op - p ` E)"
     by (auto simp add: F_def)
-  then have "setprod id F = setprod (op - p) E"
+  then have "prod id F = prod (op - p) E"
     apply simp
     apply (insert finite_E inj_on_pminusx_E)
-    apply (frule setprod.reindex [of "minus p" E id])
+    apply (frule prod.reindex [of "minus p" E id])
     apply auto
     done
   then have one:
-    "[setprod id F = setprod (StandardRes p o (op - p)) E] (mod p)"
+    "[prod id F = prod (StandardRes p o (op - p)) E] (mod p)"
     apply simp
     apply (insert p_g_0 finite_E StandardRes_prod)
     by (auto)
@@ -409,20 +409,20 @@
     apply (rule_tac b = "p - x" in zcong_trans, auto)
     done
   ultimately have c:
-    "[setprod (StandardRes p o (op - p)) E = setprod (uminus) E](mod p)"
+    "[prod (StandardRes p o (op - p)) E = prod (uminus) E](mod p)"
     apply simp
     using finite_E p_g_0
-      setprod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
+      prod_same_function_zcong [of E "StandardRes p o (op - p)" uminus p]
     by auto
-  then have two: "[setprod id F = setprod (uminus) E](mod p)"
+  then have two: "[prod id F = prod (uminus) E](mod p)"
     apply (insert one c)
-    apply (rule zcong_trans [of "setprod id F"
-                               "setprod (StandardRes p o op - p) E" p
-                               "setprod uminus E"], auto)
+    apply (rule zcong_trans [of "prod id F"
+                               "prod (StandardRes p o op - p) E" p
+                               "prod uminus E"], auto)
     done
-  also have "setprod uminus E = (setprod id E) * (-1)^(card E)"
+  also have "prod uminus E = (prod id E) * (-1)^(card E)"
     using finite_E by (induct set: finite) auto
-  then have "setprod uminus E = (-1) ^ (card E) * (setprod id E)"
+  then have "prod uminus E = (-1) ^ (card E) * (prod id E)"
     by (simp add: mult.commute)
   with two show ?thesis
     by simp
@@ -431,52 +431,52 @@
 
 subsection \<open>Gauss' Lemma\<close>
 
-lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
+lemma aux: "prod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = prod id A * a ^ card A"
   by (auto simp add: finite_E neg_one_special)
 
 theorem pre_gauss_lemma:
   "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
 proof -
-  have "[setprod id A = setprod id F * setprod id D](mod p)"
-    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: setprod.strong_cong)
-  then have "[setprod id A = ((-1)^(card E) * setprod id E) *
-      setprod id D] (mod p)"
-    by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: setprod.strong_cong)
-  then have "[setprod id A = ((-1)^(card E) * setprod id C)] (mod p)"
+  have "[prod id A = prod id F * prod id D](mod p)"
+    by (auto simp add: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
+  then have "[prod id A = ((-1)^(card E) * prod id E) *
+      prod id D] (mod p)"
+    by (rule zcong_trans) (auto simp add: prod_F_zcong zcong_scalar cong del: prod.strong_cong)
+  then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
     apply (rule zcong_trans)
     apply (insert C_prod_eq_D_times_E, erule subst)
     apply (subst mult.assoc)
     apply auto
     done
-  then have "[setprod id A = ((-1)^(card E) * setprod id B)] (mod p)"
+  then have "[prod id A = ((-1)^(card E) * prod id B)] (mod p)"
     apply (rule zcong_trans)
-    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: setprod.strong_cong)
+    apply (simp add: C_B_zcong_prod zcong_scalar2 cong del: prod.strong_cong)
     done
-  then have "[setprod id A = ((-1)^(card E) *
-    (setprod id ((%x. x * a) ` A)))] (mod p)"
+  then have "[prod id A = ((-1)^(card E) *
+    (prod id ((%x. x * a) ` A)))] (mod p)"
     by (simp add: B_def)
-  then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))]
+  then have "[prod id A = ((-1)^(card E) * (prod (%x. x * a) A))]
     (mod p)"
-    by (simp add:finite_A inj_on_xa_A setprod.reindex cong del: setprod.strong_cong)
-  moreover have "setprod (%x. x * a) A =
-    setprod (%x. a) A * setprod id A"
+    by (simp add:finite_A inj_on_xa_A prod.reindex cong del: prod.strong_cong)
+  moreover have "prod (%x. x * a) A =
+    prod (%x. a) A * prod id A"
     using finite_A by (induct set: finite) auto
-  ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A *
-    setprod id A))] (mod p)"
+  ultimately have "[prod id A = ((-1)^(card E) * (prod (%x. a) A *
+    prod id A))] (mod p)"
     by simp
-  then have "[setprod id A = ((-1)^(card E) * a^(card A) *
-      setprod id A)](mod p)"
-    by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A setprod_constant mult.assoc)
-  then have a: "[setprod id A * (-1)^(card E) =
-      ((-1)^(card E) * a^(card A) * setprod id A * (-1)^(card E))](mod p)"
+  then have "[prod id A = ((-1)^(card E) * a^(card A) *
+      prod id A)](mod p)"
+    by (rule zcong_trans) (simp add: zcong_scalar2 zcong_scalar finite_A prod_constant mult.assoc)
+  then have a: "[prod id A * (-1)^(card E) =
+      ((-1)^(card E) * a^(card A) * prod id A * (-1)^(card E))](mod p)"
     by (rule zcong_scalar)
-  then have "[setprod id A * (-1)^(card E) = setprod id A *
+  then have "[prod id A * (-1)^(card E) = prod id A *
       (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
     by (rule zcong_trans) (simp add: a mult.commute mult.left_commute)
-  then have "[setprod id A * (-1)^(card E) = setprod id A *
+  then have "[prod id A * (-1)^(card E) = prod id A *
       a^(card A)](mod p)"
-    by (rule zcong_trans) (simp add: aux cong del: setprod.strong_cong)
-  with this zcong_cancel2 [of p "setprod id A" "(- 1) ^ card E" "a ^ card A"]
+    by (rule zcong_trans) (simp add: aux cong del: prod.strong_cong)
+  with this zcong_cancel2 [of p "prod id A" "(- 1) ^ card E" "a ^ card A"]
       p_g_0 A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
     by (simp add: order_less_imp_le)
   from this show ?thesis
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Int2.thy
--- a/src/HOL/Old_Number_Theory/Int2.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Int2.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -170,7 +170,7 @@
   done
 
 lemma all_relprime_prod_relprime: "[| finite A; \<forall>x \<in> A. zgcd x y = 1 |]
-    ==> zgcd (setprod id A) y = 1"
+    ==> zgcd (prod id A) y = 1"
   by (induct set: finite) (auto simp add: zgcd_zgcd_zmult)
 
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -561,7 +561,7 @@
 
 lemma nproduct_mod:
   assumes fS: "finite S" and n0: "n \<noteq> 0"
-  shows "[setprod (\<lambda>m. a(m) mod n) S = setprod a S] (mod n)"
+  shows "[prod (\<lambda>m. a(m) mod n) S = prod a S] (mod n)"
 proof-
   have th1:"[1 = 1] (mod n)" by (simp add: modeq_def)
   from cong_mult
@@ -569,17 +569,17 @@
     [x1 = x2] (mod n) \<and> [y1 = y2] (mod n) \<longrightarrow> [x1 * y1 = x2 * y2] (mod n)"
     by blast
   have th4:"\<forall>x\<in>S. [a x mod n = a x] (mod n)" by (simp add: modeq_def)
-  from setprod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS)
+  from prod.related [where h="(\<lambda>m. a(m) mod n)" and g=a, OF th1 th3 fS, OF th4] show ?thesis by (simp add: fS)
 qed
 
 lemma nproduct_cmul:
   assumes fS:"finite S"
-  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
-unfolding setprod.distrib setprod_constant [of c] ..
+  shows "prod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * prod a S"
+unfolding prod.distrib prod_constant [of c] ..
 
 lemma coprime_nproduct:
   assumes fS: "finite S" and Sn: "\<forall>x\<in>S. coprime n (a x)"
-  shows "coprime n (setprod a S)"
+  shows "coprime n (prod a S)"
   using fS by (rule finite_subset_induct)
     (insert Sn, auto simp add: coprime_mul)
 
@@ -607,7 +607,7 @@
       let ?h = "\<lambda>m. (a * m) mod n"
       
       have eq0: "(\<Prod>i\<in>?S. ?h i) = (\<Prod>i\<in>?S. i)"
-      proof (rule setprod.reindex_bij_betw)
+      proof (rule prod.reindex_bij_betw)
         have "inj_on (\<lambda>i. ?h i) ?S"
         proof (rule inj_onI)
           fix x y assume "?h x = ?h y"
@@ -636,7 +636,7 @@
       have "[(\<Prod>i\<in>?S. a * i) = (\<Prod>i\<in>?S. ?h i)] (mod n)"
         by (simp add: cong_commute)
       also have "[(\<Prod>i\<in>?S. ?h i) = ?P] (mod n)"
-        using eq0 fS an by (simp add: setprod_def modeq_def)
+        using eq0 fS an by (simp add: prod_def modeq_def)
       finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
         unfolding cardfS mult.commute[of ?P "a^ (card ?S)"]
           nproduct_cmul[OF fS, symmetric] mult_1_right by simp
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/Residues.thy
--- a/src/HOL/Old_Number_Theory/Residues.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/Residues.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -147,7 +147,7 @@
   by (auto simp add: zcong_zmod)
 
 lemma StandardRes_prod: "[| finite X; 0 < m |] 
-     ==> [setprod f X = setprod (StandardRes m o f) X] (mod m)"
+     ==> [prod f X = prod (StandardRes m o f) X] (mod m)"
   apply (rule_tac F = X in finite_induct)
   apply (auto intro!: zcong_zmult simp add: StandardRes_prop1)
   done
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/WilsonBij.thy
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -229,9 +229,9 @@
     apply (subgoal_tac [2] "a = 1 \<or> a = p - 1")
      apply (rule_tac [3] zcong_square_zless)
         apply auto
-  apply (subst setprod.insert)
+  apply (subst prod.insert)
     prefer 3
-    apply (subst setprod.insert)
+    apply (subst prod.insert)
       apply (auto simp add: fin_bijER)
   apply (subgoal_tac "zcong ((a * b) * \<Prod>A) (1 * 1) p")
    apply (simp add: mult.assoc)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -247,8 +247,8 @@
    prefer 2
    apply (subst wset.simps)
    apply (auto, unfold Let_def, auto)
-  apply (subst setprod.insert)
-    apply (tactic \<open>stac @{context} @{thm setprod.insert} 3\<close>)
+  apply (subst prod.insert)
+    apply (tactic \<open>stac @{context} @{thm prod.insert} 3\<close>)
       apply (subgoal_tac [5]
         "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
        prefer 5
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Probability/Central_Limit_Theorem.thy
--- a/src/HOL/Probability/Central_Limit_Theorem.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Probability/Central_Limit_Theorem.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -64,7 +64,7 @@
       apply auto
       done
     also have "\<dots> = (\<psi> n t)^n"
-      by (auto simp add: * setprod_constant)
+      by (auto simp add: * prod_constant)
     finally have \<phi>_eq: "\<phi> n t =(\<psi> n t)^n" .
 
     have "norm (\<psi> n t - (1 - ?t^2 * \<sigma>\<^sup>2 / 2)) \<le> ?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Probability/Independent_Family.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -166,7 +166,7 @@
               also have "\<dots> = prob (A j) * (\<Prod>i\<in>J-{j}. prob (A i))"
                 using \<open>A j = X\<close> by simp
               also have "\<dots> = (\<Prod>i\<in>J. prob (A i))"
-                unfolding setprod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob  (A i)"]
+                unfolding prod.insert_remove[OF \<open>finite J\<close>, symmetric, of "\<lambda>i. prob  (A i)"]
                 using \<open>j \<in> J\<close> by (simp add: insert_absorb)
               finally show ?thesis .
             qed
@@ -207,7 +207,7 @@
             have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = (\<Prod>i\<in>insert j J. prob ((A(j := X)) i))"
               using J A \<open>j \<in> K\<close> by (intro indep_setsD[OF G']) auto
             then have "prob (\<Inter>i\<in>insert j J. (A(j := X)) i) = prob X * (\<Prod>i\<in>J. prob (A i))"
-              using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: setprod.cong) }
+              using \<open>finite J\<close> \<open>j \<notin> J\<close> by (auto intro!: prod.cong) }
           ultimately have "prob ((\<Inter>j\<in>J. A j) \<inter> (space M - X)) = (prob (space M) - prob X) * (\<Prod>i\<in>J. prob (A i))"
             by (simp add: field_simps)
           also have "\<dots> = prob (space M - X) * (\<Prod>i\<in>J. prob (A i))"
@@ -233,7 +233,7 @@
           qed
           moreover { fix k
             from J A \<open>j \<in> K\<close> have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * (\<Prod>i\<in>J. prob (A i))"
-              by (subst indep_setsD[OF F(2)]) (auto intro!: setprod.cong split: if_split_asm)
+              by (subst indep_setsD[OF F(2)]) (auto intro!: prod.cong split: if_split_asm)
             also have "\<dots> = prob (F k) * prob (\<Inter>i\<in>J. A i)"
               using J A \<open>j \<in> K\<close> by (subst indep_setsD[OF G(1)]) auto
             finally have "prob (\<Inter>i\<in>insert j J. (A(j := F k)) i) = prob (F k) * prob (\<Inter>i\<in>J. A i)" . }
@@ -478,9 +478,9 @@
       also have "\<dots> = (\<Prod>l\<in>(\<Union>k\<in>K. L k). prob (?E' l))"
         using L K E' by (intro indep_setsD[OF indep]) (simp_all add: UN_mono)
       also have "\<dots> = (\<Prod>j\<in>K. \<Prod>l\<in>L j. prob (E' j l))"
-        using K L L_inj by (subst setprod.UNION_disjoint) auto
+        using K L L_inj by (subst prod.UNION_disjoint) auto
       also have "\<dots> = (\<Prod>j\<in>K. prob (A j))"
-        using K L E' by (auto simp add: A intro!: setprod.cong indep_setsD[OF indep, symmetric]) blast
+        using K L E' by (auto simp add: A intro!: prod.cong indep_setsD[OF indep, symmetric]) blast
       finally show "prob (\<Inter>j\<in>K. A j) = (\<Prod>j\<in>K. prob (A j))" .
     qed
   next
@@ -849,8 +849,8 @@
     with indep have "prob (\<Inter>j\<in>I. ?A j) = (\<Prod>j\<in>I. prob (?A j))"
       by auto
     also have "\<dots> = (\<Prod>j\<in>J. prob (A j))"
-      unfolding if_distrib setprod.If_cases[OF \<open>finite I\<close>]
-      using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 setprod.neutral_const)
+      unfolding if_distrib prod.If_cases[OF \<open>finite I\<close>]
+      using prob_space \<open>J \<subseteq> I\<close> by (simp add: Int_absorb1 prod.neutral_const)
     finally show "prob (\<Inter>j\<in>J. A j) = (\<Prod>j\<in>J. prob (A j))" ..
   qed
 qed
@@ -1007,7 +1007,7 @@
   finally show ?thesis .
 qed
 
-lemma (in prob_space) indep_vars_setprod:
+lemma (in prob_space) indep_vars_prod:
   fixes X :: "'i \<Rightarrow> 'a \<Rightarrow> real"
   assumes I: "finite I" "i \<notin> I" and indep: "indep_vars (\<lambda>_. borel) X (insert i I)"
   shows "indep_var borel (X i) borel (\<lambda>\<omega>. \<Prod>i\<in>I. X i \<omega>)"
@@ -1092,7 +1092,7 @@
         using J \<open>I \<noteq> {}\<close> measurable_space[OF rv] by (auto simp: prod_emb_def PiE_iff split: if_split_asm)
       also have "emeasure M (\<Inter>i\<in>J. X i -` Y i \<inter> space M) = (\<Prod> i\<in>J. emeasure M (X i -` Y i \<inter> space M))"
         using \<open>indep_vars M' X I\<close> J \<open>I \<noteq> {}\<close> using indep_varsD[of M' X I J]
-        by (auto simp: emeasure_eq_measure setprod_ennreal measure_nonneg setprod_nonneg)
+        by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
       also have "\<dots> = (\<Prod> i\<in>J. emeasure (?D' i) (Y i))"
         using rv J by (simp add: emeasure_distr)
       also have "\<dots> = emeasure ?P' E"
@@ -1133,7 +1133,7 @@
         using rv J Y by (simp add: emeasure_distr)
       finally have "emeasure M (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. emeasure M (Y' i))" .
       then show "prob (\<Inter>j\<in>J. Y' j) = (\<Prod> i\<in>J. prob (Y' i))"
-        by (auto simp: emeasure_eq_measure setprod_ennreal measure_nonneg setprod_nonneg)
+        by (auto simp: emeasure_eq_measure prod_ennreal measure_nonneg prod_nonneg)
     qed
   qed
 qed
@@ -1283,15 +1283,15 @@
     by (rule indep_vars_cong[THEN iffD1, OF _ _ _ I(2)]) (auto simp: Y_def)
 
   have "(\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. X i \<omega>) \<partial>M) = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. Y i \<omega>) \<partial>M)"
-    using I(3) by (auto intro!: nn_integral_cong setprod.cong simp add: Y_def max_def)
+    using I(3) by (auto intro!: nn_integral_cong prod.cong simp add: Y_def max_def)
   also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x))"
     by (subst nn_integral_distr) auto
   also have "\<dots> = (\<integral>\<^sup>+\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
     unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
   also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<^sup>+\<omega>. \<omega> \<partial>distr M borel (Y i)))"
-    by (rule product_nn_integral_setprod) (auto intro: \<open>finite I\<close>)
+    by (rule product_nn_integral_prod) (auto intro: \<open>finite I\<close>)
   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<^sup>+\<omega>. X i \<omega> \<partial>M)"
-    by (intro setprod.cong nn_integral_cong) (auto simp: nn_integral_distr Y_def rv_X)
+    by (intro prod.cong nn_integral_cong) (auto simp: nn_integral_distr Y_def rv_X)
   finally show ?thesis .
 qed (simp add: emeasure_space_1)
 
@@ -1330,15 +1330,15 @@
   also have "\<dots> = (\<integral>\<omega>. (\<Prod>i\<in>I. \<omega> i) \<partial>Pi\<^sub>M I (\<lambda>i. distr M borel (Y i)))"
     unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y] ..
   also have "\<dots> = (\<Prod>i\<in>I. (\<integral>\<omega>. \<omega> \<partial>distr M borel (Y i)))"
-    by (rule product_integral_setprod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y)
+    by (rule product_integral_prod) (auto intro: \<open>finite I\<close> simp: integrable_distr_eq int_Y)
   also have "\<dots> = (\<Prod>i\<in>I. \<integral>\<omega>. X i \<omega> \<partial>M)"
-    by (intro setprod.cong integral_cong)
+    by (intro prod.cong integral_cong)
        (auto simp: integral_distr Y_def rv_X)
   finally show ?eq .
 
   have "integrable (distr M (Pi\<^sub>M I (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>I. Y i x)) (\<lambda>\<omega>. (\<Prod>i\<in>I. \<omega> i))"
     unfolding indep_vars_iff_distr_eq_PiM[THEN iffD1, OF \<open>I \<noteq> {}\<close> rv_Y indep_Y]
-    by (intro product_integrable_setprod[OF \<open>finite I\<close>])
+    by (intro product_integrable_prod[OF \<open>finite I\<close>])
        (simp add: integrable_distr_eq int_Y)
   then show ?int
     by (simp add: integrable_distr_eq Y_def)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -98,7 +98,7 @@
   shows "measure (PiM I M) (emb I J (Pi\<^sub>E J X)) = (\<Prod> i\<in>J. measure (M i) (X i))"
   using emeasure_PiM_emb[OF assms]
   unfolding emeasure_eq_measure M.emeasure_eq_measure
-  by (simp add: setprod_ennreal measure_nonneg setprod_nonneg)
+  by (simp add: prod_ennreal measure_nonneg prod_nonneg)
 
 lemma sets_Collect_single':
   "i \<in> I \<Longrightarrow> {x\<in>space (M i). P x} \<in> sets (M i) \<Longrightarrow> {x\<in>space (PiM I M). P (x i)} \<in> sets (PiM I M)"
@@ -151,7 +151,7 @@
   have "emeasure (Pi\<^sub>M I M) (prod_emb I M J (Pi\<^sub>E J A)) = emeasure (Pi\<^sub>M I ?M) (P.emb I J (Pi\<^sub>E J A))"
     by (auto simp: prod_emb_def PiE_iff intro!: arg_cong2[where f=emeasure] PiM_cong)
   also have "\<dots> = (\<Prod>i\<in>J. emeasure (M i) (A i))"
-    using J A by (subst P.emeasure_PiM_emb[OF J]) (auto intro!: setprod.cong)
+    using J A by (subst P.emeasure_PiM_emb[OF J]) (auto intro!: prod.cong)
   finally show ?thesis .
 qed
 
@@ -173,7 +173,7 @@
   have "Pi\<^sub>M (insert i' I) M ?X = (\<Prod>i\<in>J. M i (A i))"
     using M J A by (intro emeasure_PiM_emb) auto
   also have "\<dots> = M i' (if i' \<in> J then (A i') else space (M i')) * (\<Prod>i\<in>J-{i'}. M i (A i))"
-    using setprod.insert_remove[of J "\<lambda>i. M i (A i)" i'] J M'.emeasure_space_1
+    using prod.insert_remove[of J "\<lambda>i. M i (A i)" i'] J M'.emeasure_space_1
     by (cases "i' \<in> J") (auto simp: insert_absorb)
   also have "(\<Prod>i\<in>J-{i'}. M i (A i)) = Pi\<^sub>M I M (prod_emb I M (J - {i'}) (Pi\<^sub>E (J - {i'}) A))"
     using M J A by (intro emeasure_PiM_emb[symmetric]) auto
@@ -205,7 +205,7 @@
   have "?I (prod_emb I (\<lambda>i. M (f i)) J (Pi\<^sub>E J A)) = (\<Prod>j\<in>J. M (f j) (A j))"
     using f J A by (intro emeasure_PiM_emb M) auto
   also have "\<dots> = (\<Prod>j\<in>f`J. M j (A (the_inv_into I f j)))"
-    using f J by (subst setprod.reindex) (auto intro!: setprod.cong intro: inj_on_subset simp: the_inv_into_f_f)
+    using f J by (subst prod.reindex) (auto intro!: prod.cong intro: inj_on_subset simp: the_inv_into_f_f)
   also have "\<dots> = ?K (prod_emb K M (f`J) (\<Pi>\<^sub>E j\<in>f`J. A (the_inv_into I f j)))"
     using f J A by (intro emeasure_PiM_emb[symmetric] M) (auto simp: the_inv_into_f_f)
   also have "prod_emb K M (f`J) (\<Pi>\<^sub>E j\<in>f`J. A (the_inv_into I f j)) = ?t -` prod_emb I (\<lambda>i. M (f i)) J (Pi\<^sub>E J A) \<inter> space ?K"
@@ -352,12 +352,12 @@
   also have "emeasure S ?F = (\<Prod>j\<in>(op + i) -` J. emeasure M (E (i + j)))"
     using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI inj_on_def)
   also have "\<dots> = (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j))"
-    by (rule setprod.reindex_cong [of "\<lambda>x. x - i"])
+    by (rule prod.reindex_cong [of "\<lambda>x. x - i"])
        (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
   also have "emeasure S ?E = (\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j))"
     using J by (intro emeasure_PiM_emb) simp_all
   also have "(\<Prod>j\<in>J \<inter> {..<i}. emeasure M (E j)) * (\<Prod>j\<in>J - (J \<inter> {..<i}). emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
-    by (subst mult.commute) (auto simp: J setprod.subset_diff[symmetric])
+    by (subst mult.commute) (auto simp: J prod.subset_diff[symmetric])
   finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
 qed simp_all
 
@@ -383,10 +383,10 @@
   also have "emeasure S ?F = (\<Prod>j\<in>Suc -` J. emeasure M (E (Suc j)))"
     using J by (intro emeasure_PiM_emb) (simp_all add: finite_vimageI)
   also have "\<dots> = (\<Prod>j\<in>J - {0}. emeasure M (E j))"
-    by (rule setprod.reindex_cong [of "\<lambda>x. x - 1"])
+    by (rule prod.reindex_cong [of "\<lambda>x. x - 1"])
        (auto simp: image_iff Bex_def not_less nat_eq_diff_eq ac_simps cong: conj_cong intro!: inj_onI)
   also have "emeasure M ?E * (\<Prod>j\<in>J - {0}. emeasure M (E j)) = (\<Prod>j\<in>J. emeasure M (E j))"
-    by (auto simp: M.emeasure_space_1 setprod.remove J)
+    by (auto simp: M.emeasure_space_1 prod.remove J)
   finally show "emeasure ?D ?X = (\<Prod>j\<in>J. emeasure M (E j))" .
 qed simp_all
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -485,7 +485,7 @@
 sublocale finite_product_prob_space \<subseteq> prob_space "\<Pi>\<^sub>M i\<in>I. M i"
 proof
   show "emeasure (\<Pi>\<^sub>M i\<in>I. M i) (space (\<Pi>\<^sub>M i\<in>I. M i)) = 1"
-    by (simp add: measure_times M.emeasure_space_1 setprod.neutral_const space_PiM)
+    by (simp add: measure_times M.emeasure_space_1 prod.neutral_const space_PiM)
 qed
 
 lemma (in finite_product_prob_space) prob_times:
@@ -497,8 +497,8 @@
   also have "\<dots> = (\<Prod>i\<in>I. emeasure (M i) (X i))"
     using measure_times X by simp
   also have "\<dots> = ennreal (\<Prod>i\<in>I. measure (M i) (X i))"
-    using X by (simp add: M.emeasure_eq_measure setprod_ennreal measure_nonneg)
-  finally show ?thesis by (simp add: measure_nonneg setprod_nonneg)
+    using X by (simp add: M.emeasure_eq_measure prod_ennreal measure_nonneg)
+  finally show ?thesis by (simp add: measure_nonneg prod_nonneg)
 qed
 
 subsection \<open>Distributions\<close>
@@ -1201,8 +1201,8 @@
     apply (subst emeasure_distr)
     apply (auto intro!: sets_PiM_I_finite simp: Pi_iff)
     apply (subst emeasure_PiM)
-    apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> setprod.reindex[OF \<open>inj_on t J\<close>]
-      if_distrib[where f="emeasure (M _)"] setprod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
+    apply (auto simp: the_inv_into_f_f \<open>inj_on t J\<close> prod.reindex[OF \<open>inj_on t J\<close>]
+      if_distrib[where f="emeasure (M _)"] prod.If_cases emeasure_space_1 Int_absorb1 \<open>t`J \<subseteq> K\<close>)
     done
 qed simp
 
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -83,7 +83,7 @@
 lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
   by auto
 
-lemma setprod_sum_distrib_lists:
+lemma prod_sum_distrib_lists:
   fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
   shows "(\<Sum>ms\<in>{ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
          (\<Prod>i<n. \<Sum>m\<in>{m\<in>S. P i m}. f m)"
@@ -100,7 +100,7 @@
   show ?case unfolding *
     using Suc[of "\<lambda>i. P (Suc i)"]
     by (simp add: sum.reindex split_conv sum_cartesian_product'
-      lessThan_Suc_eq_insert_0 setprod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
+      lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
 qed
 
 declare space_point_measure[simp]
@@ -169,12 +169,12 @@
     case (Suc n)
     then show ?case
       by (simp add: lists_length_Suc_eq lessThan_Suc_eq_insert_0
-                    sum.reindex setprod.reindex)
+                    sum.reindex prod.reindex)
   qed
   then show "sum P msgs = 1"
     unfolding msgs_def P_def by simp
   fix x
-  have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: setprod_nonneg)
+  have "\<And> A f. 0 \<le> (\<Prod>x\<in>A. M (f x))" by (auto simp: prod_nonneg)
   then show "0 \<le> P x"
     unfolding P_def by (auto split: prod.split simp: zero_le_mult_iff)
 qed auto
@@ -255,8 +255,8 @@
     apply (simp add: \<mu>'_eq)
     apply (simp add: * P_def)
     apply (simp add: sum_cartesian_product')
-    using setprod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
-    by (auto simp add: sum_distrib_left[symmetric] subset_eq setprod.neutral_const)
+    using prod_sum_distrib_lists[OF M.finite_space, of M n "\<lambda>x x. True"] \<open>k \<in> keys\<close>
+    by (auto simp add: sum_distrib_left[symmetric] subset_eq prod.neutral_const)
 qed
 
 lemma fst_image_msgs[simp]: "fst`msgs = keys"
@@ -352,14 +352,14 @@
           (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)"
         unfolding P_def using \<open>K k \<noteq> 0\<close> \<open>k \<in> keys\<close>
         apply (simp add: sum_cartesian_product' sum_divide_distrib msgs_def ** cong: conj_cong)
-        apply (subst setprod_sum_distrib_lists[OF M.finite_space]) ..
+        apply (subst prod_sum_distrib_lists[OF M.finite_space]) ..
       finally have "(\<P>(OB ; fst) {(obs, k)}) / K k =
             (\<Prod>i<n. \<Sum>m\<in>{m\<in>messages. observe k m = obs ! i}. M m)" . }
     note * = this
 
     have "(\<P>(OB ; fst) {(obs, k)}) / K k = (\<P>(OB ; fst) {(obs', k)}) / K k"
       unfolding *[OF obs] *[OF obs']
-      using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: setprod.reindex)
+      using t_f(1) obs_t_f by (subst (2) t_f(2)) (simp add: prod.reindex)
     then have "(\<P>(OB ; fst) {(obs, k)}) = (\<P>(OB ; fst) {(obs', k)})"
       using \<open>K k \<noteq> 0\<close> by auto }
   note t_eq_imp = this
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Rat.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -701,7 +701,7 @@
 lemma of_rat_sum: "of_rat (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>A. of_rat (f a))"
   by (induct rule: infinite_finite_induct) (auto simp: of_rat_add)
 
-lemma of_rat_setprod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"
+lemma of_rat_prod: "of_rat (\<Prod>a\<in>A. f a) = (\<Prod>a\<in>A. of_rat (f a))"
   by (induct rule: infinite_finite_induct) (auto simp: of_rat_mult)
 
 lemma nonzero_of_rat_inverse: "a \<noteq> 0 \<Longrightarrow> of_rat (inverse a) = inverse (of_rat a)"
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -319,7 +319,7 @@
 lemma of_real_sum[simp]: "of_real (sum f s) = (\<Sum>x\<in>s. of_real (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
-lemma of_real_setprod[simp]: "of_real (setprod f s) = (\<Prod>x\<in>s. of_real (f x))"
+lemma of_real_prod[simp]: "of_real (prod f s) = (\<Prod>x\<in>s. of_real (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
 lemma nonzero_of_real_inverse:
@@ -501,10 +501,10 @@
   then show ?case by (metis Reals_0 sum.infinite)
 qed simp_all
 
-lemma setprod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> setprod f s \<in> \<real>"
+lemma prod_in_Reals [intro,simp]: "(\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>) \<Longrightarrow> prod f s \<in> \<real>"
 proof (induct s rule: infinite_finite_induct)
   case infinite
-  then show ?case by (metis Reals_1 setprod.infinite)
+  then show ?case by (metis Reals_1 prod.infinite)
 qed simp_all
 
 lemma Reals_induct [case_names of_real, induct set: Reals]:
@@ -978,20 +978,20 @@
     by simp
 qed
 
-lemma setprod_norm: "setprod (\<lambda>x. norm (f x)) A = norm (setprod f A)"
+lemma prod_norm: "prod (\<lambda>x. norm (f x)) A = norm (prod f A)"
   for f :: "'a \<Rightarrow> 'b::{comm_semiring_1,real_normed_div_algebra}"
   by (induct A rule: infinite_finite_induct) (auto simp: norm_mult)
 
-lemma norm_setprod_le:
-  "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))"
+lemma norm_prod_le:
+  "norm (prod f A) \<le> (\<Prod>a\<in>A. norm (f a :: 'a :: {real_normed_algebra_1,comm_monoid_mult}))"
 proof (induct A rule: infinite_finite_induct)
   case empty
   then show ?case by simp
 next
   case (insert a A)
-  then have "norm (setprod f (insert a A)) \<le> norm (f a) * norm (setprod f A)"
+  then have "norm (prod f (insert a A)) \<le> norm (f a) * norm (prod f A)"
     by (simp add: norm_mult_ineq)
-  also have "norm (setprod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
+  also have "norm (prod f A) \<le> (\<Prod>a\<in>A. norm (f a))"
     by (rule insert)
   finally show ?case
     by (simp add: insert mult_left_mono)
@@ -1000,7 +1000,7 @@
   then show ?case by simp
 qed
 
-lemma norm_setprod_diff:
+lemma norm_prod_diff:
   fixes z w :: "'i \<Rightarrow> 'a::{real_normed_algebra_1, comm_monoid_mult}"
   shows "(\<And>i. i \<in> I \<Longrightarrow> norm (z i) \<le> 1) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> norm (w i) \<le> 1) \<Longrightarrow>
     norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) \<le> (\<Sum>i\<in>I. norm (z i - w i))"
@@ -1020,9 +1020,9 @@
   also have "norm ?t1 \<le> norm (\<Prod>i\<in>I. z i) * norm (z i - w i)"
     by (rule norm_mult_ineq)
   also have "\<dots> \<le> (\<Prod>i\<in>I. norm (z i)) * norm(z i - w i)"
-    by (rule mult_right_mono) (auto intro: norm_setprod_le)
+    by (rule mult_right_mono) (auto intro: norm_prod_le)
   also have "(\<Prod>i\<in>I. norm (z i)) \<le> (\<Prod>i\<in>I. 1)"
-    by (intro setprod_mono) (auto intro!: insert)
+    by (intro prod_mono) (auto intro!: insert)
   also have "norm ?t2 \<le> norm ((\<Prod>i\<in>I. z i) - (\<Prod>i\<in>I. w i)) * norm (w i)"
     by (rule norm_mult_ineq)
   also have "norm (w i) \<le> 1"
@@ -1042,9 +1042,9 @@
   shows "norm (z^m - w^m) \<le> m * norm (z - w)"
 proof -
   have "norm (z^m - w^m) = norm ((\<Prod> i < m. z) - (\<Prod> i < m. w))"
-    by (simp add: setprod_constant)
+    by (simp add: prod_constant)
   also have "\<dots> \<le> (\<Sum>i<m. norm (z - w))"
-    by (intro norm_setprod_diff) (auto simp add: assms)
+    by (intro norm_prod_diff) (auto simp add: assms)
   also have "\<dots> = m * norm (z - w)"
     by simp
   finally show ?thesis .
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -2018,41 +2018,41 @@
 subsection \<open>Products indexed over intervals\<close>
 
 syntax (ASCII)
-  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<_./ _)" [0,0,10] 10)
-  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<=_./ _)" [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<_./ _)" [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<=_./ _)" [0,0,10] 10)
 
 syntax (latex_prod output)
-  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
-  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
-  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
-  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
 
 syntax
-  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_<_./ _)" [0,0,10] 10)
-  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+  "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+  "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
 
 translations
-  "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..b}"
-  "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..<b}"
-  "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..n}"
-  "\<Prod>i<n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..<n}"
-
-lemma setprod_int_plus_eq: "setprod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
+  "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..b}"
+  "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST prod (\<lambda>x. t) {a..<b}"
+  "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}"
+  "\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}"
+
+lemma prod_int_plus_eq: "prod int {i..i+j} =  \<Prod>{int i..int (i+j)}"
   by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
 
-lemma setprod_int_eq: "setprod int {i..j} =  \<Prod>{int i..int j}"
+lemma prod_int_eq: "prod int {i..j} =  \<Prod>{int i..int j}"
 proof (cases "i \<le> j")
   case True
   then show ?thesis
-    by (metis le_iff_add setprod_int_plus_eq)
+    by (metis le_iff_add prod_int_plus_eq)
 next
   case False
   then show ?thesis
@@ -2062,37 +2062,37 @@
 
 subsubsection \<open>Shifting bounds\<close>
 
-lemma setprod_shift_bounds_nat_ivl:
-  "setprod f {m+k..<n+k} = setprod (%i. f(i + k)){m..<n::nat}"
+lemma prod_shift_bounds_nat_ivl:
+  "prod f {m+k..<n+k} = prod (%i. f(i + k)){m..<n::nat}"
 by (induct "n", auto simp:atLeastLessThanSuc)
 
-lemma setprod_shift_bounds_cl_nat_ivl:
-  "setprod f {m+k..n+k} = setprod (%i. f(i + k)){m..n::nat}"
-  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
-
-corollary setprod_shift_bounds_cl_Suc_ivl:
-  "setprod f {Suc m..Suc n} = setprod (%i. f(Suc i)){m..n}"
-by (simp add:setprod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
-
-corollary setprod_shift_bounds_Suc_ivl:
-  "setprod f {Suc m..<Suc n} = setprod (%i. f(Suc i)){m..<n}"
-by (simp add:setprod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-
-lemma setprod_lessThan_Suc: "setprod f {..<Suc n} = setprod f {..<n} * f n"
+lemma prod_shift_bounds_cl_nat_ivl:
+  "prod f {m+k..n+k} = prod (%i. f(i + k)){m..n::nat}"
+  by (rule prod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
+
+corollary prod_shift_bounds_cl_Suc_ivl:
+  "prod f {Suc m..Suc n} = prod (%i. f(Suc i)){m..n}"
+by (simp add:prod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+
+corollary prod_shift_bounds_Suc_ivl:
+  "prod f {Suc m..<Suc n} = prod (%i. f(Suc i)){m..<n}"
+by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
+
+lemma prod_lessThan_Suc: "prod f {..<Suc n} = prod f {..<n} * f n"
   by (simp add: lessThan_Suc mult.commute)
 
-lemma setprod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
+lemma prod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
   by (induction n) (simp_all add: lessThan_Suc mult_ac)
 
-lemma setprod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> setprod f {a..<Suc b} = setprod f {a..<b} * f b"
+lemma prod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> prod f {a..<Suc b} = prod f {a..<b} * f b"
   by (simp add: atLeastLessThanSuc mult.commute)
 
-lemma setprod_nat_ivl_Suc':
+lemma prod_nat_ivl_Suc':
   assumes "m \<le> Suc n"
-  shows   "setprod f {m..Suc n} = f (Suc n) * setprod f {m..n}"
+  shows   "prod f {m..Suc n} = f (Suc n) * prod f {m..n}"
 proof -
   from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
-  also have "setprod f \<dots> = f (Suc n) * setprod f {m..n}" by simp
+  also have "prod f \<dots> = f (Suc n) * prod f {m..n}" by simp
   finally show ?thesis .
 qed
 
@@ -2133,13 +2133,13 @@
     by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def)
 qed
 
-lemma setprod_atLeastAtMost_code:
-  "setprod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
+lemma prod_atLeastAtMost_code:
+  "prod f {a..b} = fold_atLeastAtMost_nat (\<lambda>a acc. f a * acc) a b 1"
 proof -
   have "comp_fun_commute (\<lambda>a. op * (f a))"
     by unfold_locales (auto simp: o_def mult_ac)
   thus ?thesis
-    by (simp add: setprod.eq_fold fold_atLeastAtMost_nat o_def)
+    by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
 qed
 
 (* TODO: Add support for more kinds of intervals here *)
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Transcendental.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -35,7 +35,7 @@
   by (metis of_nat_fact of_real_of_nat_eq)
 
 lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
-  by (simp add: pochhammer_setprod)
+  by (simp add: pochhammer_prod)
 
 lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n"
 proof -
@@ -1522,7 +1522,7 @@
 corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
   by (simp add: exp_of_nat_mult)
 
-lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = setprod (\<lambda>x. exp (f x)) I"
+lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
   by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
 
 lemma exp_divide_power_eq:
@@ -1744,9 +1744,9 @@
   for x :: real
   by (rule ln_unique) (simp add: exp_add)
 
-lemma ln_setprod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i > 0) \<Longrightarrow> ln (setprod f I) = sum (\<lambda>x. ln(f x)) I"
+lemma ln_prod: "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i > 0) \<Longrightarrow> ln (prod f I) = sum (\<lambda>x. ln(f x)) I"
   for f :: "'a \<Rightarrow> real"
-  by (induct I rule: finite_induct) (auto simp: ln_mult setprod_pos)
+  by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
 
 lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   for x :: real
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/ex/Birthday_Paradox.thy
--- a/src/HOL/ex/Birthday_Paradox.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/ex/Birthday_Paradox.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -64,11 +64,11 @@
     by (auto intro!: finite_PiE)
   have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
   from assms this finite subset show ?thesis
-    by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
+    by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on prod_constant)
 qed
 
-lemma setprod_upto_nat_unfold:
-  "setprod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * setprod f {m..(n - 1)}))"
+lemma prod_upto_nat_unfold:
+  "prod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * prod f {m..(n - 1)}))"
   by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
 
 section \<open>Birthday paradox\<close>
@@ -81,7 +81,7 @@
   from assms show ?thesis
     using card_PiE[OF \<open>finite S\<close>, of "\<lambda>i. T"] \<open>finite S\<close>
       card_extensional_funcset_not_inj_on[OF \<open>finite S\<close> \<open>finite T\<close> \<open>card S <= card T\<close>]
-    by (simp add: fact_div_fact setprod_upto_nat_unfold setprod_constant)
+    by (simp add: fact_div_fact prod_upto_nat_unfold prod_constant)
 qed
 
 end
diff -r c939cc16b605 -r f76b6dda2e56 src/HOL/ex/Sum_of_Powers.thy
--- a/src/HOL/ex/Sum_of_Powers.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -23,8 +23,8 @@
 next
   case (Suc l)
   have "of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
-    using setprod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
-    by (simp add: ac_simps setprod.atLeast0_lessThan_Suc_shift)
+    using prod.atLeast0_lessThan_Suc [where ?'a = 'a, symmetric, of "\<lambda>i. of_nat (Suc n - i)" k]
+    by (simp add: ac_simps prod.atLeast0_lessThan_Suc_shift)
   also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (Suc n - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
     by (simp add: Suc atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
   also have "... = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
@@ -32,7 +32,7 @@
   finally have "(\<Prod>i=0..<k. of_nat (n - i)) = (of_nat :: (nat \<Rightarrow> 'a)) (n + 1 - k) / of_nat (n + 1) * (\<Prod>i=0..<k. of_nat (Suc n - i))"
     by (simp add: field_simps)
   with assms show ?thesis
-    by (simp add: binomial_altdef_of_nat setprod_dividef)
+    by (simp add: binomial_altdef_of_nat prod_dividef)
 qed
 
 lemma real_binomial_eq_mult_binomial_Suc: