# HG changeset patch
# User wenzelm
# Date 1451493918 -3600
# Node ID 6b780867d4260848197afd451f4f699ec46e884c
# Parent  d68b705719ce657f25f5d1188139e34b59867fbe
clarified syntax;

diff -r d68b705719ce -r 6b780867d426 src/ZF/AC.thy
--- a/src/ZF/AC.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -25,7 +25,7 @@
 apply (erule bspec, assumption)
 done
 
-lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi> X \<in> Pow(C)-{0}. X)"
+lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Prod>X \<in> Pow(C)-{0}. X)"
 apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
 apply (erule_tac [2] exI, blast)
 done
@@ -51,7 +51,7 @@
 apply (erule_tac [2] fun_weaken_type, blast+)
 done
 
-lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi> x \<in> A. x)"
+lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Prod>x \<in> A. x)"
 apply (rule AC_Pi)
 apply (simp_all add: non_empty_family)
 done
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -263,7 +263,7 @@
 
 lemma AC13_AC1_lemma:
      "\<forall>B \<in> A. f(B)\<noteq>0 & f(B)<=B & f(B) \<lesssim> 1   
-      ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Pi> X \<in> A. X)"
+      ==> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)"
 apply (rule lam_type)
 apply (drule bspec, assumption)
 apply (elim conjE)
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC17_AC1.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -15,7 +15,7 @@
 (** AC0 is equivalent to AC1.  
     AC0 comes from Suppes, AC1 from Rubin & Rubin **)
 
-lemma AC0_AC1_lemma: "[| f:(\<Pi> X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Pi> X \<in> D. X)"
+lemma AC0_AC1_lemma: "[| f:(\<Prod>X \<in> A. X); D \<subseteq> A |] ==> \<exists>g. g:(\<Prod>X \<in> D. X)"
 by (fast intro!: lam_type apply_type)
 
 lemma AC0_AC1: "AC0 ==> AC1"
@@ -29,7 +29,7 @@
 
 (**** The proof of AC1 ==> AC17 ****)
 
-lemma AC1_AC17_lemma: "f \<in> (\<Pi> X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
+lemma AC1_AC17_lemma: "f \<in> (\<Prod>X \<in> Pow(A) - {0}. X) ==> f \<in> (Pow(A) - {0} -> A)"
 apply (rule Pi_type, assumption)
 apply (drule apply_type, assumption, fast)
 done
@@ -144,7 +144,7 @@
 (* ********************************************************************** *)
 
 lemma AC1_AC2_aux1:
-     "[| f:(\<Pi> X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
+     "[| f:(\<Prod>X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
 by (fast elim!: apply_type)
 
 lemma AC1_AC2_aux2: 
@@ -178,7 +178,7 @@
 
 lemma AC2_AC1_aux3:
      "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D \<inter> C = {y}   
-      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Pi> X \<in> A. X)"
+      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Prod>X \<in> A. X)"
 apply (rule lam_type)
 apply (drule bspec, blast)
 apply (blast intro: AC2_AC1_aux2 fst_type)
@@ -234,7 +234,7 @@
 (* ********************************************************************** *)
 
 lemma AC3_AC1_lemma:
-     "b\<notin>A ==> (\<Pi> x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Pi> x \<in> A. x)"
+     "b\<notin>A ==> (\<Prod>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Prod>x \<in> A. x)"
 apply (simp add: id_def cong add: Pi_cong)
 apply (rule_tac b = A in subst_context, fast)
 done
@@ -277,7 +277,7 @@
 done
 
 lemma AC5_AC4_aux4: "[| R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x |]  
-                ==> (\<lambda>x \<in> C. snd(g`x)): (\<Pi> x \<in> C. R``{x})"
+                ==> (\<lambda>x \<in> C. snd(g`x)): (\<Prod>x \<in> C. R``{x})"
 apply (rule lam_type)
 apply (force dest: apply_type)
 done
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC18_AC19.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -18,14 +18,14 @@
 (* ********************************************************************** *)
 
 lemma PROD_subsets:
-     "[| f \<in> (\<Pi> b \<in> {P(a). a \<in> A}. b);  \<forall>a \<in> A. P(a)<=Q(a) |]   
-      ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Pi> a \<in> A. Q(a))"
+     "[| f \<in> (\<Prod>b \<in> {P(a). a \<in> A}. b);  \<forall>a \<in> A. P(a)<=Q(a) |]   
+      ==> (\<lambda>a \<in> A. f`P(a)) \<in> (\<Prod>a \<in> A. Q(a))"
 by (rule lam_type, drule apply_type, auto)
 
 lemma lemma_AC18:
-     "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |] 
+     "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X)); A \<noteq> 0 |] 
       ==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> 
-          (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
+          (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
 apply (rule subsetI)
 apply (erule_tac x = "{{b \<in> B (a) . x \<in> X (a,b) }. a \<in> A}" in allE)
 apply (erule impE, fast)
@@ -68,12 +68,12 @@
 done
 
 lemma lemma1_2: 
-        "[| f`(uu(a)) \<notin> a; f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B); a \<in> A |]   
+        "[| f`(uu(a)) \<notin> a; f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B); a \<in> A |]   
                 ==> f`(uu(a))-{0} \<in> a"
 apply (unfold uu_def, fast elim!: lemma1_1 dest!: apply_type)
 done
 
-lemma lemma1: "\<exists>f. f \<in> (\<Pi> B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Pi> B \<in> A. B)"
+lemma lemma1: "\<exists>f. f \<in> (\<Prod>B \<in> {uu(a). a \<in> A}. B) ==> \<exists>f. f \<in> (\<Prod>B \<in> A. B)"
 apply (erule exE)
 apply (rule_tac x = "\<lambda>a\<in>A. if (f` (uu(a)) \<in> a, f` (uu(a)), f` (uu(a))-{0})" 
        in exI)
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC7_AC9.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -53,16 +53,16 @@
 (* the proof.                                                             *)
 (* ********************************************************************** *)
 
-lemma lemma1_1: "y \<in> (\<Pi> B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Pi> B \<in> A. B)"
+lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) ==> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)"
 by (fast intro!: lam_type snd_type apply_type)
 
 lemma lemma1_2:
-     "y \<in> (\<Pi> B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Pi> B \<in> A. Y*B)"
+     "y \<in> (\<Prod>B \<in> {Y*C. C \<in> A}. B) ==> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Prod>B \<in> A. Y*B)"
 apply (fast intro!: lam_type apply_type)
 done
 
 lemma AC7_AC6_lemma1:
-     "(\<Pi> B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
+     "(\<Prod>B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Prod>B \<in> A. B) \<noteq> 0"
 by (fast intro!: equals0I lemma1_1 lemma1_2)
 
 lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
@@ -92,7 +92,7 @@
 done
 
 lemma AC1_AC8_lemma2:
-     "[| f \<in> (\<Pi> X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
+     "[| f \<in> (\<Prod>X \<in> RepFun(A,p). X); D \<in> A |] ==> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
 apply (simp, fast elim!: apply_type)
 done
 
@@ -152,7 +152,7 @@
      "\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
       \<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
         f`<B1,B2> \<in> bij(B1, B2)   
-      ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
+      ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Prod>X \<in> A. X)"
 apply (intro lam_type snd_type fst_type)
 apply (rule apply_type [OF _ consI1]) 
 apply (fast intro!: fun_weaken_type bij_is_fun)
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -41,7 +41,7 @@
     "WO7 == \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))"
 
 definition  
-    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
+    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Prod>X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
 
 
 definition
@@ -56,28 +56,28 @@
 
 (* Axioms of Choice *)  
 definition
-    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
+    "AC0 == \<forall>A. \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)"
 
 definition
-    "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
+    "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Prod>X \<in> A. X))"
 
 definition
     "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)   
                    \<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})"
 definition
-    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
+    "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Prod>x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
 
 definition
-    "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
+    "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Prod>x \<in> domain(R). R``{x})))"
 
 definition
     "AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
 
 definition
-    "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Pi> B \<in> A. B)\<noteq>0"
+    "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Prod>B \<in> A. B)\<noteq>0"
 
 definition
-    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Pi> B \<in> A. B) \<noteq> 0"
+    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Prod>B \<in> A. B) \<noteq> 0"
 
 definition
     "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)   
@@ -123,12 +123,12 @@
 locale AC18 =
   assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
     ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
-      (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
+      (\<Union>f \<in> \<Prod>a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
   \<comment>"AC18 cannot be expressed within the object-logic"
 
 definition
     "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
-                   (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
+                   (\<Union>f \<in> (\<Prod>B \<in> A. B). \<Inter>a \<in> A. f`a))"
 
 
 
@@ -178,10 +178,10 @@
 by (blast dest!: well_ord_imp_ex1_first
                     [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
 
-lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Pi> X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0 \<notin> A |] ==> \<exists>f. f \<in> (\<Prod>X \<in> A. X)"
 by (fast elim!: first_in_B intro!: lam_type)
 
-lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
+lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f \<in> (\<Prod>X \<in> Pow(A)-{0}. X)"
 by (fast elim!: well_ord_subset [THEN ex_choice_fun])
 
 
diff -r d68b705719ce -r 6b780867d426 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/AC/HH.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -201,8 +201,8 @@
 done
 
 lemma lam_singI:
-     "f \<in> (\<Pi> X \<in> Pow(x)-{0}. F(X))   
-      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Pi> X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
+     "f \<in> (\<Prod>X \<in> Pow(x)-{0}. F(X))   
+      ==> (\<lambda>X \<in> Pow(x)-{0}. {f`X}) \<in> (\<Prod>X \<in> Pow(x)-{0}. {{z}. z \<in> F(X)})"
 by (fast del: DiffI DiffE
             intro!: lam_type singleton_eq_iff [THEN iffD2] dest: apply_type)
 
@@ -224,7 +224,7 @@
 Perhaps it could be simplified. *)
 
 lemma bijection:
-     "f \<in> (\<Pi> X \<in> Pow(x) - {0}. X) 
+     "f \<in> (\<Prod>X \<in> Pow(x) - {0}. X) 
       ==> \<exists>g. g \<in> bij(x, \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x})"
 apply (rule exI) 
 apply (rule bij_Least_HH_x [THEN bij_converse_bij])
diff -r d68b705719ce -r 6b780867d426 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Cardinal_AC.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -119,7 +119,7 @@
   assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
 proof -
   from f AC_Pi [of Y "%y. f-``{y}"]
-  obtain z where z: "z \<in> (\<Pi> y\<in>Y. f -`` {y})"  
+  obtain z where z: "z \<in> (\<Prod>y\<in>Y. f -`` {y})"  
     by (auto simp add: surj_def) (fast dest: apply_Pair)
   show ?thesis
     proof
@@ -146,7 +146,7 @@
   have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 
   assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
   hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
-  with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
+  with AC_Pi obtain f where f: "f \<in> (\<Prod>i\<in>K. inj(X(i), K))"
     by force 
   { fix z
     assume z: "z \<in> (\<Union>i\<in>K. X(i))"
diff -r d68b705719ce -r 6b780867d426 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Coind/Map.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -23,7 +23,7 @@
 
 definition
   map_owr :: "[i,i,i]=>i"  where
-   "map_owr(m,a,b) == \<Sigma> x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
+   "map_owr(m,a,b) == \<Sum>x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
 
 definition
   map_app :: "[i,i]=>i"  where
diff -r d68b705719ce -r 6b780867d426 src/ZF/Constructible/Reflection.thy
--- a/src/ZF/Constructible/Reflection.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Constructible/Reflection.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -353,8 +353,8 @@
 to be relativized.\<close>
 schematic_goal (in reflection)
      "Reflects(?Cl,
-               \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Pi> X \<in> A. X)),
-               \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Pi> X \<in> A. X)))"
+               \<lambda>A. 0\<notin>A \<longrightarrow> (\<exists>f. M(f) & f \<in> (\<Prod>X \<in> A. X)),
+               \<lambda>a A. 0\<notin>A \<longrightarrow> (\<exists>f\<in>Mset(a). f \<in> (\<Prod>X \<in> A. X)))"
 by fast
 
 end
diff -r d68b705719ce -r 6b780867d426 src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Induct/Brouwer.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -50,7 +50,7 @@
   monos Pi_mono
   type_intros le_trans [OF UN_upper_cardinal le_nat_Un_cardinal] inf_datatype_intros
 
-lemma Well_unfold: "Well(A, B) = (\<Sigma> x \<in> A. B(x) -> Well(A, B))"
+lemma Well_unfold: "Well(A, B) = (\<Sum>x \<in> A. B(x) -> Well(A, B))"
   by (fast intro!: Well.intros [unfolded Well.con_defs]
     elim: Well.cases [unfolded Well.con_defs])
 
diff -r d68b705719ce -r 6b780867d426 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/OrderArith.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -557,7 +557,7 @@
 text\<open>As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"}\<close>
 lemma Pow_Sigma_bij:
     "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
-     \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
+     \<in> bij(Pow(Sigma(A,B)), \<Prod>x \<in> A. Pow(B(x)))"
 apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
 apply (blast intro: lam_type)
 apply (blast dest: apply_type, simp_all)
diff -r d68b705719ce -r 6b780867d426 src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/UNITY/State.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -21,7 +21,7 @@
   default_val :: "i=>i"
 
 definition
-  "state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))"
+  "state == \<Prod>x \<in> var. cons(default_val(x), type_of(x))"
 
 definition
   "st0 == \<lambda>x \<in> var. default_val(x)"
diff -r d68b705719ce -r 6b780867d426 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/ZF.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -113,8 +113,8 @@
   "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
   "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
   "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi> _\<in>_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma> _\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
   "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
   "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
   "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
@@ -133,8 +133,8 @@
   "{b. x\<in>A}"    == "CONST RepFun(A, \<lambda>x. b)"
   "\<Inter>x\<in>A. B"    == "CONST Inter({B. x\<in>A})"
   "\<Union>x\<in>A. B"    == "CONST Union({B. x\<in>A})"
-  "\<Pi> x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
-  "\<Sigma> x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
+  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
+  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
   "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
   "\<forall>x\<in>A. P"    == "CONST Ball(A, \<lambda>x. P)"
   "\<exists>x\<in>A. P"    == "CONST Bex(A, \<lambda>x. P)"
diff -r d68b705719ce -r 6b780867d426 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/Zorn.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -197,14 +197,14 @@
 done
 
 lemma choice_super:
-     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<in> super(S,X)"
 apply (erule apply_type)
 apply (unfold super_def maxchain_def, blast)
 done
 
 lemma choice_not_equals:
-     "[| ch \<in> (\<Pi> X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
+     "[| ch \<in> (\<Prod>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
 apply (drule choice_super, assumption, assumption)
@@ -213,7 +213,7 @@
 
 text\<open>This justifies Definition 4.4\<close>
 lemma Hausdorff_next_exists:
-     "ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X) ==>
       \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                    next`X = if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X)"
 apply (rule_tac x="\<lambda>X\<in>Pow(S).
@@ -237,7 +237,7 @@
 text\<open>Lemma 4\<close>
 lemma TFin_chain_lemma4:
      "[| c \<in> TFin(S,next);
-         ch \<in> (\<Pi> X \<in> Pow(chain(S))-{0}. X);
+         ch \<in> (\<Prod>X \<in> Pow(chain(S))-{0}. X);
          next \<in> increasing(S);
          \<forall>X \<in> Pow(S). next`X =
                           if(X \<in> chain(S)-maxchain(S), ch`super(S,X), X) |]
@@ -364,14 +364,14 @@
 text\<open>* Defining the "next" operation for Zermelo's Theorem *\<close>
 
 lemma choice_Diff:
-     "[| ch \<in> (\<Pi> X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
+     "[| ch \<in> (\<Prod>X \<in> Pow(S) - {0}. X);  X \<subseteq> S;  X\<noteq>S |] ==> ch ` (S-X) \<in> S-X"
 apply (erule apply_type)
 apply (blast elim!: equalityE)
 done
 
 text\<open>This justifies Definition 6.1\<close>
 lemma Zermelo_next_exists:
-     "ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X) ==>
+     "ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X) ==>
            \<exists>next \<in> increasing(S). \<forall>X \<in> Pow(S).
                       next`X = (if X=S then S else cons(ch`(S-X), X))"
 apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
@@ -391,7 +391,7 @@
 
 text\<open>The construction of the injection\<close>
 lemma choice_imp_injection:
-     "[| ch \<in> (\<Pi> X \<in> Pow(S)-{0}. X);
+     "[| ch \<in> (\<Prod>X \<in> Pow(S)-{0}. X);
          next \<in> increasing(S);
          \<forall>X \<in> Pow(S). next`X = if(X=S, S, cons(ch`(S-X), X)) |]
       ==> (\<lambda> x \<in> S. \<Union>({y \<in> TFin(S,next). x \<notin> y}))
diff -r d68b705719ce -r 6b780867d426 src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/equalities.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -535,19 +535,19 @@
 by blast
 
 lemma SUM_UN_distrib1:
-     "(\<Sigma> x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sigma> x\<in>C(y). B(x))"
+     "(\<Sum>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sum>x\<in>C(y). B(x))"
 by blast
 
 lemma SUM_UN_distrib2:
-     "(\<Sigma> i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sigma> i\<in>I. C(i,j))"
+     "(\<Sum>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sum>i\<in>I. C(i,j))"
 by blast
 
 lemma SUM_Un_distrib1:
-     "(\<Sigma> i\<in>I \<union> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<union> (\<Sigma> j\<in>J. C(j))"
+     "(\<Sum>i\<in>I \<union> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<union> (\<Sum>j\<in>J. C(j))"
 by blast
 
 lemma SUM_Un_distrib2:
-     "(\<Sigma> i\<in>I. A(i) \<union> B(i)) = (\<Sigma> i\<in>I. A(i)) \<union> (\<Sigma> i\<in>I. B(i))"
+     "(\<Sum>i\<in>I. A(i) \<union> B(i)) = (\<Sum>i\<in>I. A(i)) \<union> (\<Sum>i\<in>I. B(i))"
 by blast
 
 (*First-order version of the above, for rewriting*)
@@ -555,11 +555,11 @@
 by (rule SUM_Un_distrib2)
 
 lemma SUM_Int_distrib1:
-     "(\<Sigma> i\<in>I \<inter> J. C(i)) = (\<Sigma> i\<in>I. C(i)) \<inter> (\<Sigma> j\<in>J. C(j))"
+     "(\<Sum>i\<in>I \<inter> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<inter> (\<Sum>j\<in>J. C(j))"
 by blast
 
 lemma SUM_Int_distrib2:
-     "(\<Sigma> i\<in>I. A(i) \<inter> B(i)) = (\<Sigma> i\<in>I. A(i)) \<inter> (\<Sigma> i\<in>I. B(i))"
+     "(\<Sum>i\<in>I. A(i) \<inter> B(i)) = (\<Sum>i\<in>I. A(i)) \<inter> (\<Sum>i\<in>I. B(i))"
 by blast
 
 (*First-order version of the above, for rewriting*)
@@ -567,7 +567,7 @@
 by (rule SUM_Int_distrib2)
 
 (*Cf Aczel, Non-Well-Founded Sets, page 115*)
-lemma SUM_eq_UN: "(\<Sigma> i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
+lemma SUM_eq_UN: "(\<Sum>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))"
 by blast
 
 lemma times_subset_iff:
@@ -575,7 +575,7 @@
 by blast
 
 lemma Int_Sigma_eq:
-     "(\<Sigma> x \<in> A'. B'(x)) \<inter> (\<Sigma> x \<in> A. B(x)) = (\<Sigma> x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
+     "(\<Sum>x \<in> A'. B'(x)) \<inter> (\<Sum>x \<in> A. B(x)) = (\<Sum>x \<in> A' \<inter> A. B'(x) \<inter> B(x))"
 by blast
 
 (** Domain **)
diff -r d68b705719ce -r 6b780867d426 src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Wed Dec 30 17:38:57 2015 +0100
+++ b/src/ZF/ex/Limit.thy	Wed Dec 30 17:45:18 2015 +0100
@@ -120,8 +120,8 @@
   (* Twice, constructions on cpos are more difficult. *)
   iprod     :: "i=>i"  where
     "iprod(DD) ==
-     <(\<Pi> n \<in> nat. set(DD`n)),
-      {x:(\<Pi> n \<in> nat. set(DD`n))*(\<Pi> n \<in> nat. set(DD`n)).
+     <(\<Prod>n \<in> nat. set(DD`n)),
+      {x:(\<Prod>n \<in> nat. set(DD`n))*(\<Prod>n \<in> nat. set(DD`n)).
        \<forall>n \<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
 
 definition
@@ -1071,18 +1071,18 @@
 (*----------------------------------------------------------------------*)
 
 lemma iprodI:
-    "x:(\<Pi> n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
+    "x:(\<Prod>n \<in> nat. set(DD`n)) ==> x \<in> set(iprod(DD))"
 by (simp add: set_def iprod_def)
 
 lemma iprodE:
-    "x \<in> set(iprod(DD)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
+    "x \<in> set(iprod(DD)) ==> x:(\<Prod>n \<in> nat. set(DD`n))"
 by (simp add: set_def iprod_def)
 
 (* Contains typing conditions in contrast to HOL-ST *)
 
 lemma rel_iprodI:
-    "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Pi> n \<in> nat. set(DD`n));
-       g:(\<Pi> n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
+    "[|!!n. n \<in> nat ==> rel(DD`n,f`n,g`n); f:(\<Prod>n \<in> nat. set(DD`n));
+       g:(\<Prod>n \<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)"
 by (simp add: iprod_def rel_I)
 
 lemma rel_iprodE:
@@ -1252,14 +1252,14 @@
 (*----------------------------------------------------------------------*)
 
 lemma DinfI:
-    "[|x:(\<Pi> n \<in> nat. set(DD`n));
+    "[|x:(\<Prod>n \<in> nat. set(DD`n));
        !!n. n \<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|]
      ==> x \<in> set(Dinf(DD,ee))"
 apply (simp add: Dinf_def)
 apply (blast intro: mkcpoI iprodI)
 done
 
-lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Pi> n \<in> nat. set(DD`n))"
+lemma Dinf_prod: "x \<in> set(Dinf(DD,ee)) ==> x:(\<Prod>n \<in> nat. set(DD`n))"
 apply (simp add: Dinf_def)
 apply (erule mkcpoD1 [THEN iprodE])
 done
@@ -1273,7 +1273,7 @@
 
 lemma rel_DinfI:
     "[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
-       x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
+       x:(\<Prod>n \<in> nat. set(DD`n)); y:(\<Prod>n \<in> nat. set(DD`n))|]
      ==> rel(Dinf(DD,ee),x,y)"
 apply (simp add: Dinf_def)
 apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)