diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/Distributor.thy
--- a/src/ZF/UNITY/Distributor.thy	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Distributor.thy	Thu Jun 12 16:40:59 2003 +0200
@@ -14,19 +14,18 @@
     "distr_follows(A, In, iIn, Out) ==
      (lift(In) IncreasingWrt prefix(A)/list(A)) Int
      (lift(iIn) IncreasingWrt prefix(nat)/list(nat)) Int
-     Always({s:state. ALL elt: set_of_list(s`iIn). elt < Nclients})
+     Always({s:state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})
          guarantees
-         (INT n: Nclients.
+         (\\<Inter>n \\<in> Nclients.
           lift(Out(n))
               Fols
-          (%s. sublist(s`In, 
-                       {k:nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
+          (%s. sublist(s`In, {k \\<in> nat. k<length(s`iIn) & nth(k, s`iIn) = n}))
 	  Wrt prefix(A)/list(A))"
   
  distr_allowed_acts :: [i=>i]=>i
   "distr_allowed_acts(Out) ==
    {D:program. AllowedActs(D) =
-   cons(id(state), UN G:(INT n:nat. preserves(lift(Out(n)))). Acts(G))}"
+   cons(id(state), \\<Union>G \\<in> (\\<Inter>n\\<in>nat. preserves(lift(Out(n)))). Acts(G))}"
 
   distr_spec :: [i, i, i, i =>i]=>i
   "distr_spec(A, In, iIn, Out) ==
@@ -39,12 +38,12 @@
         A :: i   (*the type of items being distributed *)
         D :: i
  assumes
-    var_assumes       "In:var & iIn:var & (ALL n. Out(n):var)"
-    all_distinct_vars "ALL n. all_distinct([In, iIn, iOut(n)])"
+    var_assumes       "In:var & iIn:var & (\\<forall>n. Out(n):var)"
+    all_distinct_vars "\\<forall>n. all_distinct([In, iIn, iOut(n)])"
     type_assumes      "type_of(In)=list(A) &  type_of(iIn)=list(nat) &
-                       (ALL n. type_of(Out(n))=list(A))"
+                       (\\<forall>n. type_of(Out(n))=list(A))"
    default_val_assumes "default_val(In)=Nil &
                         default_val(iIn)=Nil &
-                        (ALL n. default_val(Out(n))=Nil)"
+                        (\\<forall>n. default_val(Out(n))=Nil)"
    distr_spec  "D:distr_spec(A, In, iIn, Out)"
 end