author wenzelm Mon, 28 Dec 2015 19:23:15 +0100 changeset 61954 1d43f86f48be parent 61953 7247cb62406c child 61955 e96292f32c3c
more symbols;
 src/HOL/GCD.thy file | annotate | diff | comparison | revisions src/HOL/Library/Indicator_Function.thy file | annotate | diff | comparison | revisions src/HOL/MacLaurin.thy file | annotate | diff | comparison | revisions src/HOL/Metis_Examples/Big_O.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | comparison | revisions src/HOL/Probability/Lebesgue_Measure.thy file | annotate | diff | comparison | revisions src/HOL/Proofs/Extraction/Euclid.thy file | annotate | diff | comparison | revisions src/HOL/Taylor.thy file | annotate | diff | comparison | revisions src/HOL/UNITY/Comp/Alloc.thy file | annotate | diff | comparison | revisions src/HOL/UNITY/Comp/AllocImpl.thy file | annotate | diff | comparison | revisions
```--- 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)
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)
```--- 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
```
```--- 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)"
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>```
```--- 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 (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])```
```--- 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)
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)
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_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```
```--- 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)"
```--- 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)"

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)"
-  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)"
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)```
```--- 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) +```
```--- 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)*}```
```--- 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")