# HG changeset patch
# User wenzelm
# Date 1451326995 -3600
# Node ID 1d43f86f48be3f67a85df6354fdb3a4e5fd5f397
# Parent  7247cb62406ca55d8a559cfdd1ce8fc344c9a129
more symbols;

diff -r 7247cb62406c -r 1d43f86f48be src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/GCD.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -1489,14 +1489,14 @@
     gcd_commute_int [of "n - 1" n] by auto
 
 lemma setprod_coprime_nat [rule_format]:
-    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
+    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
   apply (case_tac "finite A")
   apply (induct set: finite)
   apply (auto simp add: gcd_mult_cancel_nat)
 done
 
 lemma setprod_coprime_int [rule_format]:
-    "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
+    "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
   apply (case_tac "finite A")
   apply (induct set: finite)
   apply (auto simp add: gcd_mult_cancel_int)
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Library/Indicator_Function.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -72,7 +72,7 @@
 
 lemma setsum_indicator_eq_card:
   assumes "finite A"
-  shows "(SUM x : A. indicator B x) = card (A Int B)"
+  shows "(\<Sum>x \<in> A. indicator B x) = card (A Int B)"
   using setsum_mult_indicator[OF assms, of "%x. 1::nat"]
   unfolding card_eq_setsum by simp
 
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/MacLaurin.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -223,7 +223,7 @@
   have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
     by (auto simp add: power_mult_distrib[symmetric])
   moreover
-  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
+  have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (\<Sum>m<n. diff m 0 * h ^ m / (fact m))"
     by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
   ultimately have " h < - t \<and>
     - t < 0 \<and>
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -493,7 +493,7 @@
 
 lemma bigo_setsum_main: "\<forall>x. \<forall>y \<in> A x. 0 <= h x y \<Longrightarrow>
     \<exists>c. \<forall>x. \<forall>y \<in> A x. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
-      (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
+      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
 apply (auto simp add: bigo_def)
 apply (rule_tac x = "\<bar>c\<bar>" in exI)
 apply (subst abs_of_nonneg) back back
@@ -508,18 +508,18 @@
 
 lemma bigo_setsum1: "\<forall>x y. 0 <= h x y \<Longrightarrow>
     \<exists>c. \<forall>x y. \<bar>f x y\<bar> <= c * (h x y) \<Longrightarrow>
-      (\<lambda>x. SUM y : A x. f x y) =o O(\<lambda>x. SUM y : A x. h x y)"
+      (\<lambda>x. \<Sum>y \<in> A x. f x y) =o O(\<lambda>x. \<Sum>y \<in> A x. h x y)"
 by (metis (no_types) bigo_setsum_main)
 
 lemma bigo_setsum2: "\<forall>y. 0 <= h y \<Longrightarrow>
     \<exists>c. \<forall>y. \<bar>f y\<bar> <= c * (h y) \<Longrightarrow>
-      (\<lambda>x. SUM y : A x. f y) =o O(\<lambda>x. SUM y : A x. h y)"
+      (\<lambda>x. \<Sum>y \<in> A x. f y) =o O(\<lambda>x. \<Sum>y \<in> A x. h y)"
 apply (rule bigo_setsum1)
 by metis+
 
 lemma bigo_setsum3: "f =o O(h) \<Longrightarrow>
-    (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
-      O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
+    (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+      O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
 apply (rule bigo_setsum1)
  apply (rule allI)+
  apply (rule abs_ge_zero)
@@ -528,9 +528,9 @@
 by (metis abs_ge_zero mult.left_commute mult_left_mono)
 
 lemma bigo_setsum4: "f =o g +o O(h) \<Longrightarrow>
-    (\<lambda>x. SUM y : A x. l x y * f(k x y)) =o
-      (\<lambda>x. SUM y : A x. l x y * g(k x y)) +o
-        O(\<lambda>x. SUM y : A x. \<bar>l x y * h(k x y)\<bar>)"
+    (\<lambda>x. \<Sum>y \<in> A x. l x y * f(k x y)) =o
+      (\<lambda>x. \<Sum>y \<in> A x. l x y * g(k x y)) +o
+        O(\<lambda>x. \<Sum>y \<in> A x. \<bar>l x y * h(k x y)\<bar>)"
 apply (rule set_minus_imp_plus)
 apply (subst fun_diff_def)
 apply (subst setsum_subtractf [symmetric])
@@ -540,10 +540,10 @@
 
 lemma bigo_setsum5: "f =o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
     \<forall>x. 0 <= h x \<Longrightarrow>
-      (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
-        O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
-apply (subgoal_tac "(\<lambda>x. SUM y : A x. (l x y) * h(k x y)) =
-      (\<lambda>x. SUM y : A x. \<bar>(l x y) * h(k x y)\<bar>)")
+      (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+        O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
+apply (subgoal_tac "(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y)) =
+      (\<lambda>x. \<Sum>y \<in> A x. \<bar>(l x y) * h(k x y)\<bar>)")
  apply (erule ssubst)
  apply (erule bigo_setsum3)
 apply (rule ext)
@@ -553,9 +553,9 @@
 
 lemma bigo_setsum6: "f =o g +o O(h) \<Longrightarrow> \<forall>x y. 0 <= l x y \<Longrightarrow>
     \<forall>x. 0 <= h x \<Longrightarrow>
-      (\<lambda>x. SUM y : A x. (l x y) * f(k x y)) =o
-        (\<lambda>x. SUM y : A x. (l x y) * g(k x y)) +o
-          O(\<lambda>x. SUM y : A x. (l x y) * h(k x y))"
+      (\<lambda>x. \<Sum>y \<in> A x. (l x y) * f(k x y)) =o
+        (\<lambda>x. \<Sum>y \<in> A x. (l x y) * g(k x y)) +o
+          O(\<lambda>x. \<Sum>y \<in> A x. (l x y) * h(k x y))"
   apply (rule set_minus_imp_plus)
   apply (subst fun_diff_def)
   apply (subst setsum_subtractf [symmetric])
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -178,32 +178,32 @@
   by (induct k) (auto simp add: cong_mult_int)
 
 lemma cong_setsum_nat [rule_format]:
-    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
-      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+    "(\<forall>x\<in>A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
+      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
   apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_add_nat)
   done
 
 lemma cong_setsum_int [rule_format]:
-    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
-      [(SUM x:A. f x) = (SUM x:A. g x)] (mod m)"
+    "(\<forall>x\<in>A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
+      [(\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. g x)] (mod m)"
   apply (cases "finite A")
   apply (induct set: finite)
   apply (auto intro: cong_add_int)
   done
 
 lemma cong_setprod_nat [rule_format]:
-    "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
-      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+    "(\<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")
   apply (induct set: finite)
   apply (auto intro: cong_mult_nat)
   done
 
 lemma cong_setprod_int [rule_format]:
-    "(ALL x: A. [((f x)::int) = g x] (mod m)) \<longrightarrow>
-      [(PROD x:A. f x) = (PROD x:A. g x)] (mod m)"
+    "(\<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")
   apply (induct set: finite)
   apply (auto intro: cong_mult_int)
@@ -566,18 +566,18 @@
   by (auto simp add: cong_altdef_int lcm_least_int) [1]
 
 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
-    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-    (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
-      [x = y] (mod (PROD i:A. m i))"
+    (\<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_nat)
   done
 
 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
-    (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-    (ALL i:A. [(x::int) = y] (mod m i)) \<longrightarrow>
-      [x = y] (mod (PROD i:A. m i))"
+    (\<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_int)
@@ -758,18 +758,18 @@
     and m :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
     and cop: "ALL i : A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (PROD j : A - {i}. m j)))"
+  shows "EX b. (ALL i : A. [b i = 1] (mod m i) \<and> [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j)))"
 proof (rule finite_set_choice, rule fin, rule ballI)
   fix i
   assume "i : A"
-  with cop have "coprime (PROD j : A - {i}. m j) (m i)"
+  with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
     by (intro setprod_coprime_nat, auto)
-  then have "EX x. [(PROD j : A - {i}. m j) * x = 1] (mod m i)"
+  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 : A - {i}. m j) * x = 1] (mod m i)"
+  then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by auto
-  moreover have "[(PROD j : A - {i}. m j) * x = 0]
-    (mod (PROD j : A - {i}. m j))"
+  moreover have "[(\<Prod>j \<in> A - {i}. m j) * x = 0]
+    (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}))"
@@ -786,22 +786,22 @@
 proof -
   from chinese_remainder_aux_nat [OF fin cop] obtain b where
     bprop: "ALL i:A. [b i = 1] (mod m i) \<and>
-      [b i = 0] (mod (PROD j : A - {i}. m j))"
+      [b i = 0] (mod (\<Prod>j \<in> A - {i}. m j))"
     by blast
-  let ?x = "SUM i:A. (u i) * (b i)"
+  let ?x = "\<Sum>i\<in>A. (u i) * (b i)"
   show "?thesis"
   proof (rule exI, clarify)
     fix i
     assume a: "i : A"
     show "[?x = u i] (mod m i)"
     proof -
-      from fin a have "?x = (SUM j:{i}. u j * b j) +
-          (SUM j:A-{i}. u j * b j)"
+      from fin a have "?x = (\<Sum>j \<in> {i}. u j * b j) +
+          (\<Sum>j \<in> A - {i}. u j * b j)"
         by (subst setsum.union_disjoint [symmetric], auto intro: setsum.cong)
-      then have "[?x = u i * b i + (SUM j:A-{i}. u j * b j)] (mod m i)"
+      then have "[?x = u i * b i + (\<Sum>j \<in> A - {i}. u j * b j)] (mod m i)"
         by auto
-      also have "[u i * b i + (SUM j:A-{i}. u j * b j) =
-                  u i * 1 + (SUM j:A-{i}. u j * 0)] (mod m i)"
+      also have "[u i * b i + (\<Sum>j \<in> A - {i}. u j * b j) =
+                  u i * 1 + (\<Sum>j \<in> A - {i}. u j * 0)] (mod m i)"
         apply (rule cong_add_nat)
         apply (rule cong_scalar2_nat)
         using bprop a apply blast
@@ -822,9 +822,9 @@
 qed
 
 lemma coprime_cong_prod_nat [rule_format]: "finite A \<Longrightarrow>
-    (ALL i: A. (ALL j: A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
-      (ALL i: A. [(x::nat) = y] (mod m i)) \<longrightarrow>
-         [x = y] (mod (PROD i:A. m i))"
+    (\<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_nat)
@@ -835,17 +835,17 @@
     and m :: "'a \<Rightarrow> nat"
     and u :: "'a \<Rightarrow> nat"
   assumes fin: "finite A"
-    and nz: "ALL i:A. m i \<noteq> 0"
-    and cop: "ALL i:A. (ALL j : A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX! x. x < (PROD i:A. m i) \<and> (ALL i:A. [x = u i] (mod m i))"
+    and nz: "\<forall>i\<in>A. m i \<noteq> 0"
+    and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
+  shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
 proof -
   from chinese_remainder_nat [OF fin cop]
   obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
     by blast
-  let ?x = "y mod (PROD i:A. m i)"
-  from fin nz have prodnz: "(PROD i:A. m i) \<noteq> 0"
+  let ?x = "y mod (\<Prod>i\<in>A. m i)"
+  from fin nz have prodnz: "(\<Prod>i\<in>A. m i) \<noteq> 0"
     by auto
-  then have less: "?x < (PROD i:A. m i)"
+  then have less: "?x < (\<Prod>i\<in>A. m i)"
     by auto
   have cong: "ALL i:A. [?x = u i] (mod m i)"
     apply auto
@@ -859,11 +859,11 @@
     apply (rule fin)
     apply assumption
     done
-  have unique: "ALL z. z < (PROD i:A. m i) \<and>
+  have unique: "ALL z. z < (\<Prod>i\<in>A. m i) \<and>
       (ALL i:A. [z = u i] (mod m i)) \<longrightarrow> z = ?x"
   proof (clarify)
     fix z
-    assume zless: "z < (PROD i:A. m i)"
+    assume zless: "z < (\<Prod>i\<in>A. m i)"
     assume zcong: "(ALL i:A. [z = u i] (mod m i))"
     have "ALL i:A. [?x = z] (mod m i)"
       apply clarify
@@ -872,7 +872,7 @@
       apply (rule cong_sym_nat)
       using zcong apply auto
       done
-    with fin cop have "[?x = z] (mod (PROD i:A. m i))"
+    with fin cop have "[?x = z] (mod (\<Prod>i\<in>A. m i))"
       apply (intro coprime_cong_prod_nat)
       apply auto
       done
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -226,15 +226,15 @@
       apply (subgoal_tac "delta i > 0")
       apply arith
       by (rule deltai_gt0)
-    also have "... \<le> (SUM i : S. F(r i) - F(l i) + epsilon / 2^(i+2))"
+    also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
       apply (rule setsum_mono)
       apply simp
       apply (rule order_trans)
       apply (rule less_imp_le)
       apply (rule deltai_prop)
       by auto
-    also have "... = (SUM i : S. F(r i) - F(l i)) +
-        (epsilon / 4) * (SUM i : S. (1 / 2)^i)" (is "_ = ?t + _")
+    also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
+        (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
       by (subst setsum.distrib) (simp add: field_simps setsum_right_distrib)
     also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
       apply (rule add_left_mono)
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -123,7 +123,7 @@
   qed
 qed
 
-lemma dvd_prod [iff]: "n dvd (PROD m::nat:#mset (n # ns). m)"
+lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
   by (simp add: msetprod_Un msetprod_singleton)
 
 definition all_prime :: "nat list \<Rightarrow> bool" where
@@ -140,13 +140,13 @@
 
 lemma split_all_prime:
   assumes "all_prime ms" and "all_prime ns"
-  shows "\<exists>qs. all_prime qs \<and> (PROD m::nat:#mset qs. m) =
-    (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+  shows "\<exists>qs. all_prime qs \<and> (\<Prod>m::nat \<in># mset qs. m) =
+    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
 proof -
   from assms have "all_prime (ms @ ns)"
     by (simp add: all_prime_append)
-  moreover from assms have "(PROD m::nat:#mset (ms @ ns). m) =
-    (PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)"
+  moreover from assms have "(\<Prod>m::nat \<in># mset (ms @ ns). m) =
+    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
     by (simp add: msetprod_Un)
   ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
   then show ?thesis ..
@@ -154,11 +154,11 @@
 
 lemma all_prime_nempty_g_one:
   assumes "all_prime ps" and "ps \<noteq> []"
-  shows "Suc 0 < (PROD m::nat:#mset ps. m)"
+  shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
   using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
     (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
 
-lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = n)"
+lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
 proof (induct n rule: nat_wf_ind)
   case (1 n)
   from `Suc 0 < n`
@@ -169,21 +169,21 @@
     assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
     then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
       and kn: "k < n" and nmk: "n = m * k" by iprover
-    from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = m" by (rule 1)
-    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m::nat:#mset ps1. m) = m"
+    from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" by (rule 1)
+    then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m"
       by iprover
-    from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = k" by (rule 1)
-    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m::nat:#mset ps2. m) = k"
+    from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
+    then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
       by iprover
     from `all_prime ps1` `all_prime ps2`
-    have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) =
-      (PROD m::nat:#mset ps1. m) * (PROD m::nat:#mset ps2. m)"
+    have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) =
+      (\<Prod>m::nat \<in># mset ps1. m) * (\<Prod>m::nat \<in># mset ps2. m)"
       by (rule split_all_prime)
     with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
   next
     assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
-    moreover have "(PROD m::nat:#mset [n]. m) = n" by (simp add: msetprod_singleton)
-    ultimately have "all_prime [n] \<and> (PROD m::nat:#mset [n]. m) = n" ..
+    moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp add: msetprod_singleton)
+    ultimately have "all_prime [n] \<and> (\<Prod>m::nat \<in># mset [n]. m) = n" ..
     then show ?thesis ..
   qed
 qed
@@ -193,7 +193,7 @@
   shows "\<exists>p. prime p \<and> p dvd n"
 proof -
   from N obtain ps where "all_prime ps"
-    and prod_ps: "n = (PROD m::nat:#mset ps. m)" using factor_exists
+    and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" using factor_exists
     by simp iprover
   with N have "ps \<noteq> []"
     by (auto simp add: all_prime_nempty_g_one msetprod_empty)
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/Taylor.thy
--- a/src/HOL/Taylor.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/Taylor.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -70,7 +70,7 @@
   qed
   ultimately obtain x where 
          "a - c < x & x < 0 &
-      f (a - c + c) = (SUM m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
+      f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
         diff n (x + c) / (fact n) * (a - c) ^ n"
      by (rule Maclaurin_minus [THEN exE])
   then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -53,8 +53,8 @@
   --{*spec (1)*}
   system_safety :: "'a systemState program set"
   where "system_safety =
-     Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
-     \<le> NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
+     Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s)
+     \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}"
 
 definition
   --{*spec (2)*}
@@ -120,8 +120,8 @@
   where "alloc_safety =
          (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees
-         Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
-         \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
+         Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv)s)
+         \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}"
 
 definition
   --{*spec (8)*}
diff -r 7247cb62406c -r 1d43f86f48be src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 18:03:26 2015 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Mon Dec 28 19:23:15 2015 +0100
@@ -375,7 +375,7 @@
 
 lemma alloc_refinement_lemma:
      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
-      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
+      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
 done