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