--- 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