diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC7_AC9.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -15,13 +15,13 @@
 (*  - Sigma_fun_space_eqpoll                                              *)
 (* ********************************************************************** *)
 
-lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->Union(A)) * B \<noteq> 0"
+lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->\<Union>(A)) * B \<noteq> 0"
 by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
 
 lemma inj_lemma: 
-        "C \<in> A ==> (\<lambda>g \<in> (nat->Union(A))*C.   
+        "C \<in> A ==> (\<lambda>g \<in> (nat->\<Union>(A))*C.   
                 (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
-                \<in> inj((nat->Union(A))*C, (nat->Union(A)) ) "
+                \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
 apply (unfold inj_def)
 apply (rule CollectI)
 apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
@@ -31,7 +31,7 @@
 done
 
 lemma Sigma_fun_space_eqpoll:
-     "[| C \<in> A; 0\<notin>A |] ==> (nat->Union(A)) * C \<approx> (nat->Union(A))"
+     "[| C \<in> A; 0\<notin>A |] ==> (nat->\<Union>(A)) * C \<approx> (nat->\<Union>(A))"
 apply (rule eqpollI)
 apply (simp add: lepoll_def)
 apply (fast intro!: inj_lemma)
@@ -62,10 +62,10 @@
 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"
+     "(\<Pi> B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> 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}"
+lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
 by (blast dest: Sigma_fun_space_not0)
 
 lemma AC7_AC6: "AC7 ==> AC6"
@@ -125,8 +125,8 @@
 (* AC9 ==> AC1                                                            *)
 (* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
 (* by Rubin & Rubin. But (x * y) is not necessarily equipollent to        *)
-(* (x * y) Un {0} when y is a set of total functions acting from nat to   *)
-(* Union(A) -- therefore we have used the set (y * nat) instead of y.     *)
+(* (x * y) \<union> {0} when y is a set of total functions acting from nat to   *)
+(* \<Union>(A) -- therefore we have used the set (y * nat) instead of y.     *)
 (* ********************************************************************** *)
 
 lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X"
@@ -134,13 +134,13 @@
                  prod_commute_eqpoll) 
 
 lemma nat_lepoll_lemma:
-     "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> Union(A)) \<times> B) \<times> nat"
+     "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> \<Union>(A)) \<times> B) \<times> nat"
 by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
 
 lemma AC9_AC1_lemma1:
      "[| 0\<notin>A;  A\<noteq>0;   
-         C = {((nat->Union(A))*B)*nat. B \<in> A}  Un  
-             {cons(0,((nat->Union(A))*B)*nat). B \<in> A};  
+         C = {((nat->\<Union>(A))*B)*nat. B \<in> A}  \<union>  
+             {cons(0,((nat->\<Union>(A))*B)*nat). B \<in> A};  
          B1 \<in> C;  B2 \<in> C |]   
       ==> B1 \<approx> B2"
 by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
@@ -149,8 +149,8 @@
              intro: eqpoll_trans eqpoll_sym )
 
 lemma AC9_AC1_lemma2:
-     "\<forall>B1 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
-      \<forall>B2 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
+     "\<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)"
 apply (intro lam_type snd_type fst_type)
@@ -162,7 +162,7 @@
 apply (unfold AC1_def AC9_def)
 apply (intro allI impI)
 apply (erule allE)
-apply (case_tac "A~=0")
+apply (case_tac "A\<noteq>0")
 apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) 
 done