src/ZF/AC/DC.thy

--- a/src/ZF/AC/DC.thy	Mon May 21 14:36:24 2001 +0200
+++ b/src/ZF/AC/DC.thy	Mon May 21 14:45:52 2001 +0200
@@ -16,15 +16,15 @@
 rules
 
   DC_def  "DC(a) ==
-	     ALL X R. R<=Pow(X)*X &
-             (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
-             --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
+	     \\<forall>X R. R \\<subseteq> Pow(X)*X &
+             (\\<forall>Y \\<in> Pow(X). Y lesspoll a --> (\\<exists>x \\<in> X. <Y,x> \\<in> R)) 
+             --> (\\<exists>f \\<in> a->X. \\<forall>b<a. <f``b,f`b> \\<in> R)"
 
-  DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R) 
-                  --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
+  DC0_def "DC0 == \\<forall>A B R. R \\<subseteq> A*B & R\\<noteq>0 & range(R) \\<subseteq> domain(R) 
+                  --> (\\<exists>f \\<in> nat->domain(R). \\<forall>n \\<in> nat. <f`n,f`succ(n)>:R)"
 
   ff_def  "ff(b, X, Q, R) ==
-	   transrec(b, %c r. THE x. first(x, {x:X. <r``c, x> : R}, Q))"
+	   transrec(b, %c r. THE x. first(x, {x \\<in> X. <r``c, x> \\<in> R}, Q))"
   
 
 locale DC0_imp =
@@ -35,10 +35,10 @@
     R	:: i
 
   assumes
-    all_ex    "ALL Y:Pow(X). Y lesspoll nat --> (EX x:X. <Y, x> : R)"
+    all_ex    "\\<forall>Y \\<in> Pow(X). Y lesspoll nat --> (\\<exists>x \\<in> X. <Y, x> \\<in> R)"
 
   defines
-    XX_def    "XX == (UN n:nat. {f:n->X. ALL k:n. <f``k, f`k> : R})"
+    XX_def    "XX == (\\<Union>n \\<in> nat. {f \\<in> n->X. \\<forall>k \\<in> n. <f``k, f`k> \\<in> R})"
     RR_def    "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  
                                   & restrict(z2, domain(z1)) = z1}"
 
@@ -53,18 +53,18 @@
     allRR :: o
 
   defines
-    XX_def    "XX == (UN n:nat.
-		      {f:succ(n)->domain(R). ALL k:n. <f`k, f`succ(k)> : R})"
+    XX_def    "XX == (\\<Union>n \\<in> nat.
+		      {f \\<in> succ(n)->domain(R). \\<forall>k \\<in> n. <f`k, f`succ(k)> \\<in> R})"
     RR_def
      "RR == {<z1,z2>:Fin(XX)*XX. 
-              (domain(z2)=succ(UN f:z1. domain(f))  
-                & (ALL f:z1. restrict(z2, domain(f)) = f))
-	      | (~ (EX g:XX. domain(g)=succ(UN f:z1. domain(f))  
-                 & (ALL f:z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
+              (domain(z2)=succ(\\<Union>f \\<in> z1. domain(f))  
+                & (\\<forall>f \\<in> z1. restrict(z2, domain(f)) = f))
+	      | (~ (\\<exists>g \\<in> XX. domain(g)=succ(\\<Union>f \\<in> z1. domain(f))  
+                 & (\\<forall>f \\<in> z1. restrict(g, domain(f)) = f)) & z2={<0,x>})}"
     allRR_def
-     "allRR == ALL b<nat.
-                <f``b, f`b> :  
-                 {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(UN f:z1. domain(f))  
-                                    & (UN f:z1. domain(f)) = b  
-                                    & (ALL f:z1. restrict(z2,domain(f)) = f))}"
+     "allRR == \\<forall>b<nat.
+                <f``b, f`b> \\<in>  
+                 {<z1,z2>:Fin(XX)*XX. (domain(z2)=succ(\\<Union>f \\<in> z1. domain(f))  
+                                    & (\\<Union>f \\<in> z1. domain(f)) = b  
+                                    & (\\<forall>f \\<in> z1. restrict(z2,domain(f)) = f))}"
 end