# HG changeset patch
# User paulson
# Date 1055428859 -7200
# Node ID 57de6d68389e77f696de159e12a47f3bb7c60247
# Parent  f8ed8428b41c9c03304316e53cc8bc14e0145cfb
x-symbols (mostly)

diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/ClientImpl.ML
--- a/src/ZF/UNITY/ClientImpl.ML	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.ML	Thu Jun 12 16:40:59 2003 +0200
@@ -8,14 +8,14 @@
 Addsimps [type_assumes, default_val_assumes];
 (* This part should be automated *)
 
-Goalw [state_def] "s:state ==> s`ask:list(nat)";
+Goalw [state_def] "s \\<in> state ==> s`ask \\<in> list(nat)";
 by (dres_inst_tac [("a", "ask")] apply_type 1);
 by Auto_tac;
 qed "ask_value_type";
 AddTCs [ask_value_type];
 Addsimps [ask_value_type];
 
-Goalw [state_def] "s:state ==> s`giv:list(nat)";
+Goalw [state_def] "s \\<in> state ==> s`giv \\<in> list(nat)";
 by (dres_inst_tac [("a", "giv")] apply_type 1);
 by Auto_tac;
 qed "giv_value_type";
@@ -23,14 +23,14 @@
 Addsimps [giv_value_type];
 
 Goalw [state_def]
-"s:state ==> s`rel:list(nat)";
+"s \\<in> state ==> s`rel \\<in> list(nat)";
 by (dres_inst_tac [("a", "rel")] apply_type 1);
 by Auto_tac;
 qed "rel_value_type";
 AddTCs [rel_value_type];
 Addsimps [rel_value_type];
 
-Goalw [state_def] "s:state ==> s`tok:nat";
+Goalw [state_def] "s \\<in> state ==> s`tok \\<in> nat";
 by (dres_inst_tac [("a", "tok")] apply_type 1);
 by Auto_tac;
 qed "tok_value_type";
@@ -39,7 +39,7 @@
 
 (** The Client Program **)
 
-Goalw [client_prog_def] "client_prog:program";
+Goalw [client_prog_def] "client_prog \\<in> program";
 by (Simp_tac 1);
 qed "client_type";
 Addsimps [client_type];
@@ -52,14 +52,14 @@
 Addsimps (map simp_of_act [client_rel_act_def, 
 client_tok_act_def, client_ask_act_def]);
 
-Goal "ALL G:program. (client_prog ok G) <-> \
-\  (G:preserves(lift(rel)) & G:preserves(lift(ask)) & \
-\   G:preserves(lift(tok)) &  client_prog:Allowed(G))";
+Goal "\\<forall>G \\<in> program. (client_prog ok G) <-> \
+\  (G \\<in> preserves(lift(rel)) & G \\<in> preserves(lift(ask)) & \
+\   G \\<in> preserves(lift(tok)) &  client_prog \\<in> Allowed(G))";
 by (auto_tac (claset(), 
      simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed]));  
 qed "client_prog_ok_iff";
 
-Goal "client_prog:(INT x:var-{ask, rel, tok}. preserves(lift(x)))";
+Goal "client_prog:(\\<Inter>x \\<in> var-{ask, rel, tok}. preserves(lift(x)))";
 by (rtac Inter_var_DiffI 1);
 by (rtac ballI 2);
 by (rtac preservesI 2);
@@ -98,10 +98,10 @@
 With no Substitution Axiom, we must prove the two invariants simultaneously. *)
 
 Goal 
-"[| client_prog ok G; G:program |]\
+"[| client_prog ok G; G \\<in> program |]\
 \     ==> client_prog Join G :  \
-\             Always({s:state. s`tok le NbT}  Int  \
-\                     {s:state. ALL elt:set_of_list(s`ask). elt le NbT})";
+\             Always({s \\<in> state. s`tok le NbT}  Int  \
+\                     {s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})";
 by (rotate_tac ~1 1);
 by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff]));
 by (rtac (invariantI RS stable_Join_Always2) 1);
@@ -122,8 +122,8 @@
 (* Export version, with no mention of tok in the postcondition, but
   unfortunately tok must be declared local.*)
 Goal 
-"client_prog: program guarantees \
-\            Always({s:state. ALL elt: set_of_list(s`ask). elt le NbT})";
+"client_prog \\<in> program guarantees \
+\            Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`ask). elt le NbT})";
 by (rtac guaranteesI 1);
 by (etac (ask_Bounded_lemma RS Always_weaken) 1);
 by Auto_tac;
@@ -132,25 +132,25 @@
 (*** Towards proving the liveness property ***)
 
 Goal 
-"client_prog: stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+"client_prog \\<in> stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
 by (constrains_tac 1);
 by Auto_tac;
 qed "client_prog_stable_rel_le_giv";
 
 Goal
-"[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
-\   ==> client_prog Join G:  Stable({s:state. <s`rel, s`giv>:prefix(nat)})";
+"[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
+\   ==> client_prog Join G \\<in> Stable({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
 by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1);
 by (auto_tac (claset(), simpset() addsimps [lift_def]));
 qed "client_prog_Join_Stable_rel_le_giv";
 
-Goal "[| client_prog Join G: Incr(lift(giv)); G:preserves(lift(rel)) |] \
-\   ==> client_prog Join G : Always({s:state. <s`rel, s`giv>:prefix(nat)})";
+Goal "[| client_prog Join G \\<in> Incr(lift(giv)); G \\<in> preserves(lift(rel)) |] \
+\   ==> client_prog Join G  \\<in> Always({s \\<in> state. <s`rel, s`giv>:prefix(nat)})";
 by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv], 
             simpset()) 1);
 qed "client_prog_Join_Always_rel_le_giv";
 
-Goal "xs:list(A) ==> xs@[a]=xs --> False";
+Goal "xs \\<in> list(A) ==> xs@[a]=xs --> False";
 by (etac list.induct 1);
 by Auto_tac;
 qed "list_app_lemma";
@@ -164,8 +164,8 @@
 qed "act_subset";
 
 Goal 
-"client_prog: \
-\ transient({s:state. s`rel = k & <k, h>:strict_prefix(nat) \
+"client_prog \\<in> \
+\ transient({s \\<in> state. s`rel = k & <k, h>:strict_prefix(nat) \
 \  & <h, s`giv>:prefix(nat) & h pfixGe s`ask})";
 by (res_inst_tac [("act", "client_rel_act")] transientI 1);
 by (simp_tac (simpset() addsimps 
@@ -186,7 +186,7 @@
 by (blast_tac (claset() addIs [lt_trans2, prefix_length_le,
                                strict_prefix_length_lt]) 1);
 by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1);
-by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(subgoal_tac "h \\<in> list(nat)"));
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
 by (auto_tac (claset(), 
               simpset() addsimps [prefix_def, Ge_def]));
@@ -203,11 +203,11 @@
 qed "strict_prefix_is_prefix";
 
 Goal 
-"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] \
-\ ==> client_prog Join G: \
-\ {s:state. s`rel = k & <k,h>:strict_prefix(nat) \
+"[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
+\ ==> client_prog Join G \\<in> \
+\ {s \\<in> state. s`rel = k & <k,h>:strict_prefix(nat) \
 \  & <h , s`giv>:prefix(nat) & h pfixGe s`ask}  \
-\       LeadsTo {s:state. <k, s`rel>:strict_prefix(nat) \
+\       LeadsTo {s \\<in> state. <k, s`rel>:strict_prefix(nat) \
 \                         & <s`rel, s`giv>:prefix(nat) & \
 \                                 <h, s`giv>:prefix(nat) & \
 \               h pfixGe s`ask}";
@@ -237,12 +237,12 @@
 qed "induct_lemma";
 
 Goal 
-"[| client_prog Join G : Incr(lift(giv)); client_prog ok G; G:program |] \
-\ ==> client_prog Join G : \
-\    {s:state. <s`rel, h>:strict_prefix(nat) \
+"[| client_prog Join G  \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] \
+\ ==> client_prog Join G  \\<in> \
+\    {s \\<in> state. <s`rel, h>:strict_prefix(nat) \
 \          & <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
-\                     LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
-by (res_inst_tac [("f", "lam x:state. length(h) #- length(x`rel)")] 
+\                     LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}";
+by (res_inst_tac [("f", "\\<lambda>x \\<in> state. length(h) #- length(x`rel)")] 
                                  LessThan_induct 1);
 by (auto_tac (claset(), simpset() addsimps [vimage_def]));
 by (rtac single_LeadsTo_I 1);
@@ -258,7 +258,7 @@
 by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2);
 by (REPEAT (dtac strict_prefix_length_lt 2));
 by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2);
-by (ALLGOALS(subgoal_tac "h:list(nat)"));
+by (ALLGOALS(subgoal_tac "h \\<in> list(nat)"));
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1])));
 by (dtac less_imp_succ_add 2);
 by (dtac less_imp_succ_add 3);
@@ -272,10 +272,10 @@
 qed "rel_progress_lemma";
 
 Goal 
-"[| client_prog Join G: Incr(lift(giv)); client_prog ok G; G:program |] ==> \
-\ client_prog Join G : \
-\  {s:state. <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
-\              LeadsTo {s:state. <h, s`rel>:prefix(nat)}";
+"[| client_prog Join G \\<in> Incr(lift(giv)); client_prog ok G; G \\<in> program |] ==> \
+\ client_prog Join G  \\<in> \
+\  {s \\<in> state. <h, s`giv>:prefix(nat) & h pfixGe s`ask}  \
+\              LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)}";
 by (rtac (client_prog_Join_Always_rel_le_giv RS Always_LeadsToI) 1);
 by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS 
     LeadsTo_Un RS LeadsTo_weaken_L) 3);
@@ -289,9 +289,9 @@
 
 (*Progress property: all tokens that are given will be released*)
 Goal 
-"client_prog: Incr(lift(giv))  guarantees  \
-\     (INT h:list(nat). {s:state. <h, s`giv>:prefix(nat) &\
-\             h pfixGe s`ask} LeadsTo {s:state. <h, s`rel>:prefix(nat)})";
+"client_prog \\<in> Incr(lift(giv))  guarantees  \
+\     (\\<Inter>h \\<in> list(nat). {s \\<in> state. <h, s`giv>:prefix(nat) &\
+\             h pfixGe s`ask} LeadsTo {s \\<in> state. <h, s`rel>:prefix(nat)})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
 by (blast_tac (claset() addIs [progress_lemma]) 1);
diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy	Thu Jun 12 16:40:59 2003 +0200
@@ -36,28 +36,29 @@
   
   client_rel_act ::i
     "client_rel_act ==
-     {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
-		    &  t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
-                  nrel < length(s`giv) &
-                  nth(nrel, s`ask) le nth(nrel, s`giv)}"
+     {<s,t> \\<in> state*state.
+      \\<exists>nrel \\<in> nat. nrel = length(s`rel) &
+                   t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
+                   nrel < length(s`giv) &
+                   nth(nrel, s`ask) le nth(nrel, s`giv)}"
   
   (** Choose a new token requirement **)
-  (** Including s'=s suppresses fairness, allowing the non-trivial part
+  (** Including t=s suppresses fairness, allowing the non-trivial part
       of the action to be ignored **)
 
   client_tok_act :: i
- "client_tok_act == {<s,t>:state*state. t=s |
-		 (t = s(tok:=succ(s`tok mod NbT)))}"
+ "client_tok_act == {<s,t> \\<in> state*state. t=s |
+		     t = s(tok:=succ(s`tok mod NbT))}"
 
   client_ask_act :: i
-  "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+  "client_ask_act == {<s,t> \\<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
   
   client_prog :: i
   "client_prog ==
-   mk_program({s:state. s`tok le NbT & s`giv = Nil &
+   mk_program({s \\<in> state. s`tok le NbT & s`giv = Nil &
 	               s`ask = Nil & s`rel = Nil},
                     {client_rel_act, client_tok_act, client_ask_act},
-                   UN G: preserves(lift(rel)) Int
+                   \\<Union>G \\<in> preserves(lift(rel)) Int
 			 preserves(lift(ask)) Int
 	                 preserves(lift(tok)).  Acts(G))"
 end
\ No newline at end of file
diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/Distributor.ML
--- a/src/ZF/UNITY/Distributor.ML	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Distributor.ML	Thu Jun 12 16:40:59 2003 +0200
@@ -16,7 +16,7 @@
 Addsimps [var_assumes, default_val_assumes,  type_assumes];
 
 Goalw [state_def]
-"s:state ==> s`In:list(A)";
+"s \\<in> state ==> s`In \\<in> list(A)";
 by (dres_inst_tac [("a", "In")] apply_type 1);
 by Auto_tac;
 qed "In_value_type";
@@ -24,7 +24,7 @@
 Addsimps [In_value_type];
 
 Goalw [state_def]
-"s:state ==> s`iIn:list(nat)";
+"s \\<in> state ==> s`iIn \\<in> list(nat)";
 by (dres_inst_tac [("a", "iIn")] apply_type 1);
 by Auto_tac;
 qed "iIn_value_type";
@@ -32,7 +32,7 @@
 Addsimps [iIn_value_type];
 
 Goalw [state_def]
-"s:state ==> s`Out(n):list(A)";
+"s \\<in> state ==> s`Out(n):list(A)";
 by (dres_inst_tac [("a", "Out(n)")] apply_type 1);
 by Auto_tac;
 qed "Out_value_type";
@@ -41,7 +41,7 @@
 
 val distrib = thm "distr_spec";
 
-Goal "D:program";
+Goal "D \\<in> program";
 by (cut_facts_tac [distrib] 1);
 by (auto_tac (claset(), simpset() addsimps 
            [distr_spec_def, distr_allowed_acts_def]));
@@ -49,9 +49,9 @@
 Addsimps [D_in_program];
 AddTCs [D_in_program];
 
-Goal "G:program ==> \
+Goal "G \\<in> program ==> \
 \   D ok G <-> \
-\  ((ALL n:nat. G:preserves(lift(Out(n)))) & D:Allowed(G))";
+\  ((\\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n)))) & D \\<in> Allowed(G))";
 by (cut_facts_tac [distrib] 1);
 by (auto_tac (claset(), 
      simpset() addsimps [INT_iff, distr_spec_def, distr_allowed_acts_def, 
@@ -66,9 +66,9 @@
 Goal 
 "D : ((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 \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt<Nclients})) \
 \     guarantees \
-\         (INT n: Nclients. lift(Out(n)) IncreasingWrt \
+\         (\\<Inter>n \\<in> Nclients. lift(Out(n)) IncreasingWrt \
 \                           prefix(A)/list(A))";
 by (cut_facts_tac [D_in_program, distrib] 1);
 by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
@@ -80,17 +80,17 @@
 val state_AlwaysI2 = state_AlwaysI RS Always_weaken;
 
 Goal
-"[| ALL n:nat. G:preserves(lift(Out(n))); \
-\  D Join G:Always({s:state. \
-\         ALL elt:set_of_list(s`iIn). elt < Nclients}) |] \
+"[| \\<forall>n \\<in> nat. G \\<in> preserves(lift(Out(n))); \
+\  D Join G \\<in> Always({s \\<in> state. \
+\         \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients}) |] \
 \ ==> D Join G : Always \
-\         ({s:state. msetsum(%n. bag_of (sublist(s`In, \
-\                      {k:nat. k < length(s`iIn) &\
+\         ({s \\<in> state. msetsum(%n. bag_of (sublist(s`In, \
+\                      {k \\<in> nat. k < length(s`iIn) &\
 \                         nth(k, s`iIn)= n})), \
 \                        Nclients, A) = \
 \             bag_of(sublist(s`In, length(s`iIn)))})";
 by (cut_facts_tac [D_in_program] 1);
-by (subgoal_tac "G:program" 1);
+by (subgoal_tac "G \\<in> program" 1);
 by (blast_tac (claset() addDs [preserves_type RS subsetD]) 2);
 by (etac ([asm_rl, state_AlwaysI2] MRS (Always_Diff_Un_eq RS iffD1)) 1);
 by Auto_tac;
@@ -100,7 +100,7 @@
 by (Asm_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [set_of_list_conv_nth]) 1); 
 by (subgoal_tac
-    "(UN i: Nclients. {k:nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
+    "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iIn) & nth(k, x`iIn) = i}) = \
 \    length(x`iIn)" 1);
 by (Asm_simp_tac 1);
 by (resolve_tac [equalityI] 1);
@@ -119,9 +119,9 @@
 Goal
  "D : ((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 \\<in> state. \\<forall>elt \\<in> set_of_list(s`iIn). elt < Nclients})) \
 \     guarantees  \
-\      (INT n: Nclients. \
+\      (\\<Inter>n \\<in> Nclients. \
 \       (%s. msetsum(%i. bag_of(s`Out(i)),  Nclients, A)) \
 \       Fols \
 \       (%s. bag_of(sublist(s`In, length(s`iIn)))) \
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
diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/Merge.ML
--- a/src/ZF/UNITY/Merge.ML	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Merge.ML	Thu Jun 12 16:40:59 2003 +0200
@@ -15,7 +15,7 @@
 Addsimps [var_assumes, default_val_assumes,  type_assumes];
 
 Goalw [state_def]
-"s:state ==> s`In(n):list(A)";
+"s \\<in> state ==> s`In(n):list(A)";
 by (dres_inst_tac [("a", "In(n)")] apply_type 1);
 by Auto_tac;
 qed "In_value_type";
@@ -23,7 +23,7 @@
 Addsimps [In_value_type];
 
 Goalw [state_def]
-"s:state ==> s`Out:list(A)";
+"s \\<in> state ==> s`Out \\<in> list(A)";
 by (dres_inst_tac [("a", "Out")] apply_type 1);
 by Auto_tac;
 qed "Out_value_type";
@@ -31,7 +31,7 @@
 Addsimps [Out_value_type];
 
 Goalw [state_def]
-"s:state ==> s`iOut:list(nat)";
+"s \\<in> state ==> s`iOut \\<in> list(nat)";
 by (dres_inst_tac [("a", "iOut")] apply_type 1);
 by Auto_tac;
 qed "Out_value_type";
@@ -41,7 +41,7 @@
 
 val merge = thm "merge_spec";
 
-Goal "M:program";
+Goal "M \\<in> program";
 by (cut_facts_tac [merge] 1);
 by (auto_tac (claset() addDs [guarantees_type RS subsetD], 
               simpset() addsimps [merge_spec_def, merge_increasing_def]));
@@ -58,20 +58,20 @@
 qed "merge_Allowed";
 
 Goal 
-"G:program ==> \
-\ M ok G <-> (G:preserves(lift(Out)) &  \
-\      G:preserves(lift(iOut)) & M:Allowed(G))";
+"G \\<in> program ==> \
+\ M ok G <-> (G \\<in> preserves(lift(Out)) &  \
+\      G \\<in> preserves(lift(iOut)) & M \\<in> Allowed(G))";
 by (cut_facts_tac [merge] 1); 
 by (auto_tac (claset(), simpset() 
          addsimps [merge_Allowed, ok_iff_Allowed]));  
 qed "M_ok_iff";
 
 Goal
-"[| G:preserves(lift(Out)); G:preserves(lift(iOut)); \
-\  M:Allowed(G) |] ==> \
-\ M Join G:Always({s:state. length(s`Out)=length(s`iOut)})";
+"[| G \\<in> preserves(lift(Out)); G \\<in> preserves(lift(iOut)); \
+\  M \\<in> Allowed(G) |] ==> \
+\ M Join G \\<in> Always({s \\<in> state. length(s`Out)=length(s`iOut)})";
 by (ftac (preserves_type RS subsetD) 1);
-by (subgoal_tac "G:program" 1);
+by (subgoal_tac "G \\<in> program" 1);
 by (assume_tac 2);
 by (ftac M_ok_iff 1);
 by (cut_facts_tac [merge] 1);
@@ -80,9 +80,9 @@
 qed "merge_Always_Out_eq_iOut";
 
 Goal 
-"[| G:preserves(lift(iOut)); G:preserves(lift(Out)); \
-\   M:Allowed(G) |] ==> \
-\ M Join G: Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})";
+"[| G \\<in> preserves(lift(iOut)); G \\<in> preserves(lift(Out)); \
+\   M \\<in> Allowed(G) |] ==> \
+\ M Join G: Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})";
 by (ftac (preserves_type RS subsetD) 1);
 by (ftac M_ok_iff 1);
 by (cut_facts_tac [merge] 1);
@@ -91,11 +91,11 @@
 qed "merge_Bounded";
 
 Goal 
-"[| G:preserves(lift(iOut)); \
-\   G: preserves(lift(Out)); M:Allowed(G) |] \
+"[| G \\<in> preserves(lift(iOut)); \
+\   G: preserves(lift(Out)); M \\<in> Allowed(G) |] \
 \ ==> M Join G : Always \
-\   ({s:state. msetsum(%i. bag_of(sublist(s`Out, \
-\     {k:nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
+\   ({s \\<in> state. msetsum(%i. bag_of(sublist(s`Out, \
+\     {k \\<in> nat. k < length(s`iOut) & nth(k, s`iOut)=i})), \
 \                  Nclients, A) = bag_of(s`Out)})";
 by (rtac ([[merge_Always_Out_eq_iOut, merge_Bounded] MRS Always_Int_I,
            state_AlwaysI RS Always_weaken] MRS (Always_Diff_Un_eq RS iffD1)) 1)
@@ -105,7 +105,7 @@
 by (auto_tac (claset(), simpset() 
               addsimps [nat_into_Finite, set_of_list_conv_nth])); 
 by (subgoal_tac
-    "(UN i:Nclients. {k:nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
+    "(\\<Union>i \\<in> Nclients. {k \\<in> nat. k < length(x`iOut) & nth(k, x`iOut) = i}) = length(x`iOut)" 1);
 by Auto_tac;
 by (resolve_tac [equalityI] 1);
 by (blast_tac (claset() addDs [ltD]) 1); 
@@ -121,7 +121,7 @@
 qed "merge_bag_Follows_lemma";
 
 Goal
-"M : (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
+"M : (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A)) \
 \       guarantees  \
 \ (%s. bag_of(s`Out)) Fols \
 \ (%s. msetsum(%i. bag_of(s`In(i)),Nclients, A)) Wrt MultLe(A, r)/Mult(A)";
diff -r f8ed8428b41c -r 57de6d68389e src/ZF/UNITY/Merge.thy
--- a/src/ZF/UNITY/Merge.thy	Mon Jun 02 15:02:31 2003 +0200
+++ b/src/ZF/UNITY/Merge.thy	Thu Jun 12 16:40:59 2003 +0200
@@ -20,40 +20,40 @@
   (*spec (11)*)
   merge_eq_Out :: [i, i] =>i
   "merge_eq_Out(Out, iOut) == program guarantees
-         Always({s:state. length(s`Out) = length(s`iOut)})"
+         Always({s \\<in> state. length(s`Out) = length(s`iOut)})"
 
   (*spec (12)*)
   merge_bounded :: i=>i
   "merge_bounded(iOut) == program guarantees
-         Always({s:state. ALL elt:set_of_list(s`iOut). elt<Nclients})"
+         Always({s \\<in> state. \\<forall>elt \\<in> set_of_list(s`iOut). elt<Nclients})"
   
   (*spec (13)*)
   (* Parameter A represents the type of tokens *)
   merge_follows :: [i, i=>i, i, i] =>i
     "merge_follows(A, In, Out, iOut) ==
-     (INT n:Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
+     (\\<Inter>n \\<in> Nclients. lift(In(n)) IncreasingWrt prefix(A)/list(A))
 		   guarantees
-     (INT n:Nclients. 
-        (%s. sublist(s`Out, {k:nat. k < length(s`iOut) &
+     (\\<Inter>n \\<in> Nclients. 
+        (%s. sublist(s`Out, {k \\<in> nat. k < length(s`iOut) &
                       nth(k, s`iOut) = n})) Fols lift(In(n))
          Wrt prefix(A)/list(A))"
 
   (*spec: preserves part*)
   merge_preserves :: [i=>i] =>i
-    "merge_preserves(In) == INT n:nat. preserves(lift(In(n)))"
+    "merge_preserves(In) == \\<Inter>n \\<in> nat. preserves(lift(In(n)))"
 
 (* environmental constraints*)
   merge_allowed_acts :: [i, i] =>i
   "merge_allowed_acts(Out, iOut) ==
-         {F:program. AllowedActs(F) =
-            cons(id(state), (UN G:preserves(lift(Out)) Int
-                                  preserves(lift(iOut)). Acts(G)))}"
+         {F \\<in> program. AllowedActs(F) =
+            cons(id(state), (\\<Union>G \\<in> preserves(lift(Out)) \\<inter>
+                                   preserves(lift(iOut)). Acts(G)))}"
   
   merge_spec :: [i, i =>i, i, i]=>i
   "merge_spec(A, In, Out, iOut) ==
-   merge_increasing(A, Out, iOut) Int merge_eq_Out(Out, iOut) Int
-   merge_bounded(iOut) Int  merge_follows(A, In, Out, iOut)
-   Int merge_allowed_acts(Out, iOut) Int merge_preserves(In)"
+   merge_increasing(A, Out, iOut) \\<inter> merge_eq_Out(Out, iOut) \\<inter>
+   merge_bounded(iOut) \\<inter>  merge_follows(A, In, Out, iOut)
+   \\<inter> merge_allowed_acts(Out, iOut) \\<inter> merge_preserves(In)"
 
 (** State definitions.  OUTPUT variables are locals **)
 locale Merge =
@@ -63,16 +63,16 @@
         A  :: i    (*the type of items being merged *)
         M :: i
  assumes
-    var_assumes       "(ALL n. In(n):var) & Out:var & iOut:var"
-    all_distinct_vars "ALL n. all_distinct([In(n), Out, iOut])"
-    type_assumes      "(ALL n. type_of(In(n))=list(A))&
+    var_assumes       "(\\<forall>n. In(n):var) & Out \\<in> var & iOut \\<in> var"
+    all_distinct_vars "\\<forall>n. all_distinct([In(n), Out, iOut])"
+    type_assumes      "(\\<forall>n. type_of(In(n))=list(A))&
 		       type_of(Out)=list(A) &
                        type_of(iOut)=list(nat)"
-   default_val_assumes "(ALL n. default_val(In(n))=Nil) &
+   default_val_assumes "(\\<forall>n. default_val(In(n))=Nil) &
                         default_val(Out)=Nil &
                         default_val(iOut)=Nil"
 
-   merge_spec  "M:merge_spec(A, In, Out, iOut)"
+   merge_spec  "M \\<in> merge_spec(A, In, Out, iOut)"
 end
 
   
\ No newline at end of file