diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Map.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -9,7 +9,7 @@
 
 definition
   TMap :: "[i,i] => i"  where
-   "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
+   "TMap(A,B) == {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}"
 
 definition
   PMap :: "[i,i] => i"  where
@@ -23,24 +23,24 @@
 
 definition
   map_owr :: "[i,i,i]=>i"  where
-   "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+   "map_owr(m,a,b) == \<Sigma> x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
 
 definition
   map_app :: "[i,i]=>i"  where
    "map_app(m,a) == m``{a}"
   
-lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
+lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})"
 by (unfold TMap_def, blast)
 
-lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
+lemma "{0} \<union> TMap(I,1) \<subseteq> {1} \<union> TMap(I, {0} \<union> TMap(I,1))"
 by (unfold TMap_def, blast)
 
-lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,2) \<subseteq> {1} \<union> TMap(I, {0,1} \<union> TMap(I,2))"
 by (unfold TMap_def, blast)
 
 (*A bit too slow.
-lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>  
-       {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2) \<subseteq>  
+       {1} \<union> TMap(I, {0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2))"
 by (unfold TMap_def, blast)
 *)
 
@@ -68,7 +68,7 @@
 (* Lemmas *)
 
 lemma MapQU_lemma: 
-    "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
+    "A \<subseteq> univ(X) ==> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
 apply (unfold quniv_def)
 apply (rule Pow_mono)
 apply (rule subset_trans [OF Sigma_mono product_univ])
@@ -164,7 +164,7 @@
 by (unfold map_emp_def, blast)
 
 lemma map_domain_owr: 
-  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
+  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
 apply (unfold map_owr_def)
 apply (auto simp add: domain_Sigma)
 done