# HG changeset patch
# User paulson
# Date 1044378760 -3600
# Node ID 3786b2fd680800c64032056fff8b5aea71b55384
# Parent  d643300e4fc073c940699e7bceb591a2c5ddf7d3
some x-symbols

diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -9,7 +9,7 @@
 
 Revised by Sidi Ehmety on January  2001 
 
-Added: a strong form of the <= relation (component_of) and localize 
+Added: a strong form of the \<subseteq> relation (component_of) and localize 
 
 *)
 
@@ -20,33 +20,32 @@
 instance program :: (type) ord ..
 
 defs
-  component_def:          "F <= H == EX G. F Join G = H"
-  strict_component_def:   "(F < (H::'a program)) == (F <= H & F ~= H)"
+  component_def:          "F \<le> H == \<exists>G. F Join G = H"
+  strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
 
 
 constdefs
-  component_of :: "'a program=>'a program=> bool"
+  component_of :: "'a program =>'a program=> bool"
                                     (infixl "component'_of" 50)
-  "F component_of H == EX G. F ok G & F Join G = H"
+  "F component_of H == \<exists>G. F ok G & F Join G = H"
 
   strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
                                     (infixl "strict'_component'_of" 50)
-  "F strict_component_of H == F component_of H & F~=H"
+  "F strict_component_of H == F component_of H & F\<noteq>H"
   
   preserves :: "('a=>'b) => 'a program set"
-    "preserves v == INT z. stable {s. v s = z}"
+    "preserves v == \<Inter>z. stable {s. v s = z}"
 
   localize  :: "('a=>'b) => 'a program => 'a program"
   "localize v F == mk_program(Init F, Acts F,
-			      AllowedActs F Int (UN G:preserves v. Acts G))"
+			      AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
 
   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
   "funPair f g == %x. (f x, g x)"
 
 
 subsection{*The component relation*}
-lemma componentI: 
-     "H <= F | H <= G ==> H <= (F Join G)"
+lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
 apply (unfold component_def, auto)
 apply (rule_tac x = "G Join Ga" in exI)
 apply (rule_tac [2] x = "G Join F" in exI)
@@ -54,61 +53,61 @@
 done
 
 lemma component_eq_subset: 
-     "(F <= G) =  
-      (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
+     "(F \<le> G) =  
+      (Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)"
 apply (unfold component_def)
 apply (force intro!: exI program_equalityI)
 done
 
-lemma component_SKIP [iff]: "SKIP <= F"
+lemma component_SKIP [iff]: "SKIP \<le> F"
 apply (unfold component_def)
 apply (force intro: Join_SKIP_left)
 done
 
-lemma component_refl [iff]: "F <= (F :: 'a program)"
+lemma component_refl [iff]: "F \<le> (F :: 'a program)"
 apply (unfold component_def)
 apply (blast intro: Join_SKIP_right)
 done
 
-lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
+lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
 by (auto intro!: program_equalityI simp add: component_eq_subset)
 
-lemma component_Join1: "F <= (F Join G)"
+lemma component_Join1: "F \<le> (F Join G)"
 by (unfold component_def, blast)
 
-lemma component_Join2: "G <= (F Join G)"
+lemma component_Join2: "G \<le> (F Join G)"
 apply (unfold component_def)
 apply (simp add: Join_commute, blast)
 done
 
-lemma Join_absorb1: "F<=G ==> F Join G = G"
+lemma Join_absorb1: "F \<le> G ==> F Join G = G"
 by (auto simp add: component_def Join_left_absorb)
 
-lemma Join_absorb2: "G<=F ==> F Join G = F"
+lemma Join_absorb2: "G \<le> F ==> F Join G = F"
 by (auto simp add: Join_ac component_def)
 
-lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
+lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
 by (simp add: component_eq_subset, blast)
 
-lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
+lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))"
 apply (unfold component_def)
 apply (blast intro: JN_absorb)
 done
 
-lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
+lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)"
 apply (unfold component_def)
 apply (blast intro: Join_assoc [symmetric])
 done
 
-lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
+lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)"
 apply (simp (no_asm_use) add: component_eq_subset)
 apply (blast intro!: program_equalityI)
 done
 
-lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
+lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
 by (simp add: component_eq_subset, blast)
 
-lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
+lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
 by (auto simp add: constrains_def component_eq_subset)
 
 (*Used in Guar.thy to show that programs are partially ordered*)
@@ -117,34 +116,34 @@
 
 subsection{*The preserves property*}
 
-lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
+lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
 by (unfold preserves_def, blast)
 
 lemma preserves_imp_eq: 
-     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'"
+     "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
 apply (unfold preserves_def stable_def constrains_def, force)
 done
 
 lemma Join_preserves [iff]: 
-     "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
+     "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
 apply (unfold preserves_def, auto)
 done
 
 lemma JN_preserves [iff]:
-     "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
+     "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
 apply (simp add: JN_stable preserves_def, blast)
 done
 
-lemma SKIP_preserves [iff]: "SKIP : preserves v"
+lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
 by (auto simp add: preserves_def)
 
 lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
 by (simp add:  funPair_def)
 
-lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
+lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w"
 by (auto simp add: preserves_def stable_def constrains_def, blast)
 
-(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
+(* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *)
 declare preserves_funPair [THEN eqset_imp_iff, iff]
 
 
@@ -157,20 +156,20 @@
 lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
 by (simp add: funPair_def o_def)
 
-lemma subset_preserves_o: "preserves v <= preserves (w o v)"
+lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)"
 by (force simp add: preserves_def stable_def constrains_def)
 
-lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
+lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}"
 apply (auto simp add: preserves_def stable_def constrains_def)
 apply (rename_tac s' s)
 apply (subgoal_tac "v s = v s'")
 apply (force+)
 done
 
-lemma preserves_subset_increasing: "preserves v <= increasing v"
+lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v"
 by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
 
-lemma preserves_id_subset_stable: "preserves id <= stable A"
+lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A"
 by (force simp add: preserves_def stable_def constrains_def)
 
 
@@ -183,27 +182,27 @@
 (** Some lemmas used only in Client.ML **)
 
 lemma stable_localTo_stable2:
-     "[| F : stable {s. P (v s) (w s)};    
-         G : preserves v;  G : preserves w |]                
-      ==> F Join G : stable {s. P (v s) (w s)}"
-apply (simp (no_asm_simp))
-apply (subgoal_tac "G: preserves (funPair v w) ")
+     "[| F \<in> stable {s. P (v s) (w s)};    
+         G \<in> preserves v;  G \<in> preserves w |]                
+      ==> F Join G \<in> stable {s. P (v s) (w s)}"
+apply (simp)
+apply (subgoal_tac "G \<in> preserves (funPair v w) ")
  prefer 2 apply simp 
-apply (drule_tac P1 = "split ?Q" in  preserves_subset_stable [THEN subsetD], auto)
+apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
 done
 
 lemma Increasing_preserves_Stable:
-     "[| F : stable {s. v s <= w s};  G : preserves v;        
-         F Join G : Increasing w |]                
-      ==> F Join G : Stable {s. v s <= w s}"
+     "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v;        
+         F Join G \<in> Increasing w |]                
+      ==> F Join G \<in> Stable {s. v s \<le> w s}"
 apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
 apply (blast intro: constrains_weaken)
 (*The G case remains*)
 apply (auto simp add: preserves_def stable_def constrains_def)
 apply (case_tac "act: Acts F", blast)
 (*We have a G-action, so delete assumptions about F-actions*)
-apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
-apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
+apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
+apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
 apply (subgoal_tac "v x = v xa")
 prefer 2 apply blast
 apply auto
@@ -212,12 +211,12 @@
 
 (** component_of **)
 
-(*  component_of is stronger than <= *)
-lemma component_of_imp_component: "F component_of H ==> F <= H"
+(*  component_of is stronger than \<le> *)
+lemma component_of_imp_component: "F component_of H ==> F \<le> H"
 by (unfold component_def component_of_def, blast)
 
 
-(* component_of satisfies many of the <='s properties *)
+(* component_of satisfies many of the same properties as \<le> *)
 lemma component_of_refl [simp]: "F component_of F"
 apply (unfold component_of_def)
 apply (rule_tac x = SKIP in exI, auto)
@@ -243,7 +242,7 @@
 by (simp add: localize_def)
 
 lemma localize_AllowedActs_eq [simp]: 
- "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
+ "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
 by (unfold localize_def, auto)
 
 end
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -18,65 +18,65 @@
 inductive "traces init acts"  
   intros 
          (*Initial trace is empty*)
-    Init:  "s: init ==> (s,[]) : traces init acts"
+    Init:  "s \<in> init ==> (s,[]) \<in> traces init acts"
 
-    Acts:  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
-	    ==> (s', s#evs) : traces init acts"
+    Acts:  "[| act: acts;  (s,evs) \<in> traces init acts;  (s,s'): act |]
+	    ==> (s', s#evs) \<in> traces init acts"
 
 
 consts reachable :: "'a program => 'a set"
 
 inductive "reachable F"
   intros 
-    Init:  "s: Init F ==> s : reachable F"
+    Init:  "s \<in> Init F ==> s \<in> reachable F"
 
-    Acts:  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
-	    ==> s' : reachable F"
+    Acts:  "[| act: Acts F;  s \<in> reachable F;  (s,s'): act |]
+	    ==> s' \<in> reachable F"
 
 constdefs
   Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co" 60)
-    "A Co B == {F. F : (reachable F Int A)  co  B}"
+    "A Co B == {F. F \<in> (reachable F \<inter> A)  co  B}"
 
   Unless  :: "['a set, 'a set] => 'a program set"     (infixl "Unless" 60)
-    "A Unless B == (A-B) Co (A Un B)"
+    "A Unless B == (A-B) Co (A \<union> B)"
 
   Stable     :: "'a set => 'a program set"
     "Stable A == A Co A"
 
   (*Always is the weak form of "invariant"*)
   Always :: "'a set => 'a program set"
-    "Always A == {F. Init F <= A} Int Stable A"
+    "Always A == {F. Init F \<subseteq> A} \<inter> Stable A"
 
-  (*Polymorphic in both states and the meaning of <= *)
+  (*Polymorphic in both states and the meaning of \<le> *)
   Increasing :: "['a => 'b::{order}] => 'a program set"
-    "Increasing f == INT z. Stable {s. z <= f s}"
+    "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
 
 
 subsection{*traces and reachable*}
 
 lemma reachable_equiv_traces:
-     "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
+     "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
 apply safe
 apply (erule_tac [2] traces.induct)
 apply (erule reachable.induct)
 apply (blast intro: reachable.intros traces.intros)+
 done
 
-lemma Init_subset_reachable: "Init F <= reachable F"
+lemma Init_subset_reachable: "Init F \<subseteq> reachable F"
 by (blast intro: reachable.intros)
 
 lemma stable_reachable [intro!,simp]:
-     "Acts G <= Acts F ==> G : stable (reachable F)"
+     "Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)"
 by (blast intro: stableI constrainsI reachable.intros)
 
 (*The set of all reachable states is an invariant...*)
-lemma invariant_reachable: "F : invariant (reachable F)"
+lemma invariant_reachable: "F \<in> invariant (reachable F)"
 apply (simp add: invariant_def)
 apply (blast intro: reachable.intros)
 done
 
 (*...in fact the strongest invariant!*)
-lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
+lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A"
 apply (simp add: stable_def constrains_def invariant_def)
 apply (rule subsetI)
 apply (erule reachable.induct)
@@ -86,55 +86,55 @@
 
 subsection{*Co*}
 
-(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
 lemmas constrains_reachable_Int =  
     subset_refl [THEN stable_reachable [unfolded stable_def], 
                  THEN constrains_Int, standard]
 
 (*Resembles the previous definition of Constrains*)
 lemma Constrains_eq_constrains: 
-     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
+     "A Co B = {F. F \<in> (reachable F  \<inter>  A) co (reachable F  \<inter>  B)}"
 apply (unfold Constrains_def)
 apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
 done
 
-lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
+lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_L)
 done
 
-lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
+lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A"
 apply (unfold stable_def Stable_def)
 apply (erule constrains_imp_Constrains)
 done
 
 lemma ConstrainsI: 
-    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
-     ==> F : A Co A'"
+    "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
+     ==> F \<in> A Co A'"
 apply (rule constrains_imp_Constrains)
 apply (blast intro: constrainsI)
 done
 
-lemma Constrains_empty [iff]: "F : {} Co B"
+lemma Constrains_empty [iff]: "F \<in> {} Co B"
 by (unfold Constrains_def constrains_def, blast)
 
-lemma Constrains_UNIV [iff]: "F : A Co UNIV"
+lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV"
 by (blast intro: ConstrainsI)
 
 lemma Constrains_weaken_R: 
-    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
+    "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_R)
 done
 
 lemma Constrains_weaken_L: 
-    "[| F : A Co A'; B<=A |] ==> F : B Co A'"
+    "[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken_L)
 done
 
 lemma Constrains_weaken: 
-   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
+   "[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_weaken)
 done
@@ -142,14 +142,14 @@
 (** Union **)
 
 lemma Constrains_Un: 
-    "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
+    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_Un [THEN constrains_weaken])
 done
 
 lemma Constrains_UN: 
-  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
-  shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
+  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+  shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)"
 apply (unfold Constrains_def)
 apply (rule CollectI)
 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 
@@ -159,83 +159,83 @@
 (** Intersection **)
 
 lemma Constrains_Int: 
-    "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
+    "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')"
 apply (unfold Constrains_def)
 apply (blast intro: constrains_Int [THEN constrains_weaken])
 done
 
 lemma Constrains_INT: 
-  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
-  shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
+  assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+  shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)"
 apply (unfold Constrains_def)
 apply (rule CollectI)
 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 
                 THEN constrains_weaken],   auto)
 done
 
-lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
+lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'"
 by (simp add: constrains_imp_subset Constrains_def)
 
-lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
+lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
 apply (simp add: Constrains_eq_constrains)
 apply (blast intro: constrains_trans constrains_weaken)
 done
 
 lemma Constrains_cancel:
-     "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
+     "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
 by (simp add: Constrains_eq_constrains constrains_def, blast)
 
 
 subsection{*Stable*}
 
 (*Useful because there's no Stable_weaken.  [Tanja Vos]*)
-lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
+lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
 by blast
 
-lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
+lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))"
 by (simp add: Stable_def Constrains_eq_constrains stable_def)
 
-lemma StableI: "F : A Co A ==> F : Stable A"
+lemma StableI: "F \<in> A Co A ==> F \<in> Stable A"
 by (unfold Stable_def, assumption)
 
-lemma StableD: "F : Stable A ==> F : A Co A"
+lemma StableD: "F \<in> Stable A ==> F \<in> A Co A"
 by (unfold Stable_def, assumption)
 
 lemma Stable_Un: 
-    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
+    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<union> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Un)
 done
 
 lemma Stable_Int: 
-    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
+    "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<inter> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Int)
 done
 
 lemma Stable_Constrains_Un: 
-    "[| F : Stable C; F : A Co (C Un A') |]    
-     ==> F : (C Un A) Co (C Un A')"
+    "[| F \<in> Stable C; F \<in> A Co (C \<union> A') |]    
+     ==> F \<in> (C \<union> A) Co (C \<union> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Un [THEN Constrains_weaken])
 done
 
 lemma Stable_Constrains_Int: 
-    "[| F : Stable C; F : (C Int A) Co A' |]    
-     ==> F : (C Int A) Co (C Int A')"
+    "[| F \<in> Stable C; F \<in> (C \<inter> A) Co A' |]    
+     ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
 apply (unfold Stable_def)
 apply (blast intro: Constrains_Int [THEN Constrains_weaken])
 done
 
 lemma Stable_UN: 
-    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)"
 by (simp add: Stable_def Constrains_UN) 
 
 lemma Stable_INT: 
-    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)"
 by (simp add: Stable_def Constrains_INT) 
 
-lemma Stable_reachable: "F : Stable (reachable F)"
+lemma Stable_reachable: "F \<in> Stable (reachable F)"
 by (simp add: Stable_eq_stable)
 
 
@@ -243,22 +243,22 @@
 subsection{*Increasing*}
 
 lemma IncreasingD: 
-     "F : Increasing f ==> F : Stable {s. x <= f s}"
+     "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
 by (unfold Increasing_def, blast)
 
 lemma mono_Increasing_o: 
-     "mono g ==> Increasing f <= Increasing (g o f)"
+     "mono g ==> Increasing f \<subseteq> Increasing (g o f)"
 apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
                  constrains_def)
 apply (blast intro: monoD order_trans)
 done
 
 lemma strict_IncreasingD: 
-     "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
+     "!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}"
 by (simp add: Increasing_def Suc_le_eq [symmetric])
 
 lemma increasing_imp_Increasing: 
-     "F : increasing f ==> F : Increasing f"
+     "F \<in> increasing f ==> F \<in> Increasing f"
 apply (unfold increasing_def Increasing_def)
 apply (blast intro: stable_imp_Stable)
 done
@@ -270,17 +270,17 @@
 subsection{*The Elimination Theorem*}
 
 (*The "free" m has become universally quantified! Should the premise be !!m
-instead of ALL m ?  Would make it harder to use in forward proof.*)
+instead of \<forall>m ?  Would make it harder to use in forward proof.*)
 
 lemma Elimination: 
-    "[| ALL m. F : {s. s x = m} Co (B m) |]  
-     ==> F : {s. s x : M} Co (UN m:M. B m)"
+    "[| \<forall>m. F \<in> {s. s x = m} Co (B m) |]  
+     ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)"
 by (unfold Constrains_def constrains_def, blast)
 
 (*As above, but for the trivial case of a one-variable state, in which the
   state is identified with its one variable.*)
 lemma Elimination_sing: 
-    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
+    "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)"
 by (unfold Constrains_def constrains_def, blast)
 
 
@@ -288,10 +288,10 @@
 
 (** Natural deduction rules for "Always A" **)
 
-lemma AlwaysI: "[| Init F<=A;  F : Stable A |] ==> F : Always A"
+lemma AlwaysI: "[| Init F \<subseteq> A;  F \<in> Stable A |] ==> F \<in> Always A"
 by (simp add: Always_def)
 
-lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
+lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
 by (simp add: Always_def)
 
 lemmas AlwaysE = AlwaysD [THEN conjE, standard]
@@ -299,7 +299,7 @@
 
 
 (*The set of all reachable states is Always*)
-lemma Always_includes_reachable: "F : Always A ==> reachable F <= A"
+lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A"
 apply (simp add: Stable_def Constrains_def constrains_def Always_def)
 apply (rule subsetI)
 apply (erule reachable.induct)
@@ -307,7 +307,7 @@
 done
 
 lemma invariant_imp_Always: 
-     "F : invariant A ==> F : Always A"
+     "F \<in> invariant A ==> F \<in> Always A"
 apply (unfold Always_def invariant_def Stable_def stable_def)
 apply (blast intro: constrains_imp_Constrains)
 done
@@ -316,55 +316,55 @@
     invariant_reachable [THEN invariant_imp_Always, standard]
 
 lemma Always_eq_invariant_reachable:
-     "Always A = {F. F : invariant (reachable F Int A)}"
+     "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
 apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
                  stable_def)
 apply (blast intro: reachable.intros)
 done
 
 (*the RHS is the traditional definition of the "always" operator*)
-lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
+lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}"
 by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
 
 lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
+lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
+lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)"
 apply (simp add: Always_eq_includes_reachable)
 apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 
                     invariant_includes_reachable [THEN subsetD])
 done
 
-lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
+lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B"
 by (auto simp add: Always_eq_includes_reachable)
 
 
 subsection{*"Co" rules involving Always*}
 
 lemma Always_Constrains_pre:
-     "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
+     "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
 by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
               Int_assoc [symmetric])
 
 lemma Always_Constrains_post:
-     "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
+     "F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')"
 by (simp add: Always_includes_reachable [THEN Int_absorb2] 
               Constrains_eq_constrains Int_assoc [symmetric])
 
-(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
+(* [| F \<in> Always INV;  F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
 lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
 
-(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
+(* [| F \<in> Always INV;  F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
 lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
 
 (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
 lemma Always_Constrains_weaken:
-     "[| F : Always C;  F : A Co A';    
-         C Int B <= A;   C Int A' <= B' |]  
-      ==> F : B Co B'"
+     "[| F \<in> Always C;  F \<in> A Co A';    
+         C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
+      ==> F \<in> B Co B'"
 apply (rule Always_ConstrainsI, assumption)
 apply (drule Always_ConstrainsD, assumption)
 apply (blast intro: Constrains_weaken)
@@ -373,23 +373,23 @@
 
 (** Conjoining Always properties **)
 
-lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B"
+lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
 by (auto simp add: Always_eq_includes_reachable)
 
-lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
+lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
 by (auto simp add: Always_eq_includes_reachable)
 
 lemma Always_Int_I:
-     "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)"
+     "[| F \<in> Always A;  F \<in> Always B |] ==> F \<in> Always (A \<inter> B)"
 by (simp add: Always_Int_distrib)
 
 (*Allows a kind of "implication introduction"*)
 lemma Always_Compl_Un_eq:
-     "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"
+     "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)"
 by (auto simp add: Always_eq_includes_reachable)
 
 (*Delete the nearest invariance assumption (which will be the second one
   used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F : Always A", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
 
 end
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Detects.thy
--- a/src/HOL/UNITY/Detects.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -15,47 +15,47 @@
    op_Equality :: "['a set, 'a set] => 'a set"          (infixl "<==>" 60)
    
 defs
-  Detects_def:  "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
-  Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
+  Detects_def:  "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
+  Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"
 
 
 (* Corollary from Sectiom 3.6.4 *)
 
-lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
+lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
 apply (rule LeadsTo_empty)
-apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
-apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
-apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
+apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
+apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
+apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
 apply auto
 apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
 done
 
 
 lemma Detects_Trans: 
-     "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
+     "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
 apply (unfold Detects_def Int_def)
 apply (simp (no_asm))
 apply safe
 apply (rule_tac [2] LeadsTo_Trans)
 apply auto
-apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
+apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
  apply (blast intro: Always_weaken)
 apply (simp add: Always_Int_distrib)
 done
 
-lemma Detects_refl: "F : A Detects A"
+lemma Detects_refl: "F \<in> A Detects A"
 apply (unfold Detects_def)
 apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
 done
 
-lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
+lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
 apply (unfold Equality_def)
 apply blast
 done
 
 (*Not quite antisymmetry: sets A and B agree in all reachable states *)
 lemma Detects_antisym: 
-     "[| F : A Detects B;  F : B Detects A|] ==> F : Always (A <==> B)"
+     "[| F \<in> A Detects B;  F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
 apply (unfold Detects_def Equality_def)
 apply (simp add: Always_Int_I Un_commute)
 done
@@ -64,7 +64,7 @@
 (* Theorem from Section 3.8 *)
 
 lemma Detects_Always: 
-     "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
+     "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
 apply (unfold Detects_def Equality_def)
 apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
 apply (blast dest: Always_at_FP intro: Always_weaken)
@@ -73,11 +73,11 @@
 (* Theorem from exercise 11.1 Section 11.3.1 *)
 
 lemma Detects_Imp_LeadstoEQ: 
-     "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"
+     "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
 apply (unfold Detects_def Equality_def)
 apply (rule_tac B = "B" in LeadsTo_Diff)
-prefer 2 apply (blast intro: Always_LeadsTo_weaken)
-apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
+ apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
+apply (blast intro: Always_LeadsTo_weaken)
 done
 
 
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -16,23 +16,23 @@
 
   (*MOVE to Relation.thy?*)
   Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
-    "Restrict A r == r Int (A <*> UNIV)"
+    "Restrict A r == r \<inter> (A <*> UNIV)"
 
   good_map :: "['a*'b => 'c] => bool"
-    "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)"
+    "good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
      (*Using the locale constant "f", this is  f (h (x,y))) = x*)
   
   extend_set :: "['a*'b => 'c, 'a set] => 'c set"
     "extend_set h A == h ` (A <*> UNIV)"
 
   project_set :: "['a*'b => 'c, 'c set] => 'a set"
-    "project_set h C == {x. EX y. h(x,y) : C}"
+    "project_set h C == {x. \<exists>y. h(x,y) \<in> C}"
 
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
-    "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
+    "extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
 
   project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
-    "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
+    "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),
@@ -56,7 +56,7 @@
     good_h:  "good_map h"
   defines f_def: "f z == fst (inv h z)"
       and g_def: "g z == snd (inv h z)"
-      and slice_def: "slice Z y == {x. h(x,y) : Z}"
+      and slice_def: "slice Z y == {x. h(x,y) \<in> Z}"
 
 
 (** These we prove OUTSIDE the locale. **)
@@ -65,7 +65,7 @@
 subsection{*Restrict*}
 (*MOVE to Relation.thy?*)
 
-lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)"
+lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \<in> A)"
 by (unfold Restrict_def, blast)
 
 lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
@@ -76,29 +76,29 @@
 lemma Restrict_empty [simp]: "Restrict {} r = {}"
 by (auto simp add: Restrict_def)
 
-lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A Int B) r"
+lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r"
 by (unfold Restrict_def, blast)
 
-lemma Restrict_triv: "Domain r <= A ==> Restrict A r = r"
+lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r"
 by (unfold Restrict_def, auto)
 
-lemma Restrict_subset: "Restrict A r <= r"
+lemma Restrict_subset: "Restrict A r \<subseteq> r"
 by (unfold Restrict_def, auto)
 
 lemma Restrict_eq_mono: 
-     "[| A <= B;  Restrict B r = Restrict B s |]  
+     "[| A \<subseteq> B;  Restrict B r = Restrict B s |]  
       ==> Restrict A r = Restrict A s"
 by (unfold Restrict_def, blast)
 
 lemma Restrict_imageI: 
-     "[| s : RR;  Restrict A r = Restrict A s |]  
-      ==> Restrict A r : Restrict A ` RR"
+     "[| s \<in> RR;  Restrict A r = Restrict A s |]  
+      ==> Restrict A r \<in> Restrict A ` RR"
 by (unfold Restrict_def image_def, auto)
 
-lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A Int Domain r"
+lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r"
 by blast
 
-lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A Int B)"
+lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
 by blast
 
 lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
@@ -169,19 +169,19 @@
 subsection{*@{term extend_set}: basic properties*}
 
 lemma project_set_iff [iff]:
-     "(x : project_set h C) = (EX y. h(x,y) : C)"
+     "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
 by (simp add: project_set_def)
 
-lemma extend_set_mono: "A<=B ==> extend_set h A <= extend_set h B"
+lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
 by (unfold extend_set_def, blast)
 
-lemma (in Extend) mem_extend_set_iff [iff]: "z : extend_set h A = (f z : A)"
+lemma (in Extend) mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
 apply (unfold extend_set_def)
 apply (force intro: h_f_g_eq [symmetric])
 done
 
 lemma (in Extend) extend_set_strict_mono [iff]:
-     "(extend_set h A <= extend_set h B) = (A <= B)"
+     "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
 by (unfold extend_set_def, force)
 
 lemma extend_set_empty [simp]: "extend_set h {} = {}"
@@ -198,7 +198,7 @@
 by (unfold extend_set_def, auto)
 
 lemma (in Extend) extend_set_project_set:
-     "C <= extend_set h (project_set h C)"
+     "C \<subseteq> extend_set h (project_set h C)"
 apply (unfold extend_set_def)
 apply (auto simp add: split_extended_all, blast)
 done
@@ -220,7 +220,7 @@
 by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
 
 (*Converse appears to fail*)
-lemma (in Extend) project_set_I: "!!z. z : C ==> f z : project_set h C"
+lemma (in Extend) project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
 by (auto simp add: split_extended_all)
 
 
@@ -228,31 +228,31 @@
 
 (*Because A and B could differ on the "other" part of the state, 
    cannot generalize to 
-      project_set h (A Int B) = project_set h A Int project_set h B
+      project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
 *)
 lemma (in Extend) project_set_extend_set_Int:
-     "project_set h ((extend_set h A) Int B) = A Int (project_set h B)"
+     "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
 by auto
 
 (*Unused, but interesting?*)
 lemma (in Extend) project_set_extend_set_Un:
-     "project_set h ((extend_set h A) Un B) = A Un (project_set h B)"
+     "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
 by auto
 
 lemma project_set_Int_subset:
-     "project_set h (A Int B) <= (project_set h A) Int (project_set h B)"
+     "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
 by auto
 
 lemma (in Extend) extend_set_Un_distrib:
-     "extend_set h (A Un B) = extend_set h A Un extend_set h B"
+     "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
 by auto
 
 lemma (in Extend) extend_set_Int_distrib:
-     "extend_set h (A Int B) = extend_set h A Int extend_set h B"
+     "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
 by auto
 
 lemma (in Extend) extend_set_INT_distrib:
-     "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"
+     "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
 by auto
 
 lemma (in Extend) extend_set_Diff_distrib:
@@ -260,26 +260,26 @@
 by auto
 
 lemma (in Extend) extend_set_Union:
-     "extend_set h (Union A) = (UN X:A. extend_set h X)"
+     "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
 by blast
 
 lemma (in Extend) extend_set_subset_Compl_eq:
-     "(extend_set h A <= - extend_set h B) = (A <= - B)"
+     "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
 by (unfold extend_set_def, auto)
 
 
 subsection{*@{term extend_act}*}
 
 (*Can't strengthen it to
-  ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
+  ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
   because h doesn't have to be injective in the 2nd argument*)
 lemma (in Extend) mem_extend_act_iff [iff]: 
-     "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"
+     "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
 by (unfold extend_act_def, auto)
 
 (*Converse fails: (z,z') would include actions that changed the g-part*)
 lemma (in Extend) extend_act_D: 
-     "(z, z') : extend_act h act ==> (f z, f z') : act"
+     "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
 by (unfold extend_act_def, auto)
 
 lemma (in Extend) extend_act_inverse [simp]: 
@@ -292,7 +292,7 @@
 by (unfold extend_act_def project_act_def, blast)
 
 lemma (in Extend) subset_extend_act_D: 
-     "act' <= extend_act h act ==> project_act h act' <= act"
+     "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
 by (unfold extend_act_def project_act_def, force)
 
 lemma (in Extend) inj_extend_act: "inj (extend_act h)"
@@ -305,7 +305,7 @@
 by (unfold extend_set_def extend_act_def, force)
 
 lemma (in Extend) extend_act_strict_mono [iff]:
-     "(extend_act h act' <= extend_act h act) = (act'<=act)"
+     "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
 by (unfold extend_act_def, auto)
 
 declare (in Extend) inj_extend_act [THEN inj_eq, iff]
@@ -322,7 +322,7 @@
 done
 
 lemma (in Extend) project_act_I: 
-     "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act"
+     "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
 apply (unfold project_act_def)
 apply (force simp add: split_extended_all)
 done
@@ -365,7 +365,7 @@
 lemma (in Extend) AllowedActs_project [simp]:
      "AllowedActs(project h C F) =  
         {act. Restrict (project_set h C) act  
-               : project_act h ` Restrict C ` AllowedActs F}"
+               \<in> project_act h ` Restrict C ` AllowedActs F}"
 apply (simp (no_asm) add: project_def image_iff)
 apply (subst insert_absorb)
 apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
@@ -386,14 +386,14 @@
 by auto
 
 lemma project_set_Union:
-     "project_set h (Union A) = (UN X:A. project_set h X)"
+     "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
 by blast
 
 
 (*Converse FAILS: the extended state contributing to project_set h C
   may not coincide with the one contributing to project_act h act*)
 lemma (in Extend) project_act_Restrict_subset:
-     "project_act h (Restrict C act) <=  
+     "project_act h (Restrict C act) \<subseteq>  
       Restrict (project_set h C) (project_act h act)"
 by (auto simp add: project_act_def)
 
@@ -405,7 +405,7 @@
      "project h C (extend h F) =  
       mk_program (Init F, Restrict (project_set h C) ` Acts F,  
                   {act. Restrict (project_set h C) act 
-                          : project_act h ` Restrict C ` 
+                          \<in> project_act h ` Restrict C ` 
                                      (project_act h -` AllowedActs F)})"
 apply (rule program_equalityI)
   apply simp
@@ -439,7 +439,7 @@
 done
 
 lemma (in Extend) extend_JN [simp]:
-     "extend h (JOIN I F) = (JN i:I. extend h (F i))"
+     "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
 apply (rule program_equalityI)
   apply (simp (no_asm) add: extend_set_INT_distrib)
  apply (simp add: image_UN, auto)
@@ -447,49 +447,49 @@
 
 (** These monotonicity results look natural but are UNUSED **)
 
-lemma (in Extend) extend_mono: "F <= G ==> extend h F <= extend h G"
+lemma (in Extend) extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
 by (force simp add: component_eq_subset)
 
-lemma (in Extend) project_mono: "F <= G ==> project h C F <= project h C G"
+lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
 by (simp add: component_eq_subset, blast)
 
 
 subsection{*Safety: co, stable*}
 
 lemma (in Extend) extend_constrains:
-     "(extend h F : (extend_set h A) co (extend_set h B)) =  
-      (F : A co B)"
+     "(extend h F \<in> (extend_set h A) co (extend_set h B)) =  
+      (F \<in> A co B)"
 by (simp add: constrains_def)
 
 lemma (in Extend) extend_stable:
-     "(extend h F : stable (extend_set h A)) = (F : stable A)"
+     "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
 by (simp add: stable_def extend_constrains)
 
 lemma (in Extend) extend_invariant:
-     "(extend h F : invariant (extend_set h A)) = (F : invariant A)"
+     "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
 by (simp add: invariant_def extend_stable)
 
 (*Projects the state predicates in the property satisfied by  extend h F.
   Converse fails: A and B may differ in their extra variables*)
 lemma (in Extend) extend_constrains_project_set:
-     "extend h F : A co B ==> F : (project_set h A) co (project_set h B)"
+     "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
 by (auto simp add: constrains_def, force)
 
 lemma (in Extend) extend_stable_project_set:
-     "extend h F : stable A ==> F : stable (project_set h A)"
+     "extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
 by (simp add: stable_def extend_constrains_project_set)
 
 
 subsection{*Weak safety primitives: Co, Stable*}
 
 lemma (in Extend) reachable_extend_f:
-     "p : reachable (extend h F) ==> f p : reachable F"
+     "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
 apply (erule reachable.induct)
 apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
 done
 
 lemma (in Extend) h_reachable_extend:
-     "h(s,y) : reachable (extend h F) ==> s : reachable F"
+     "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
 by (force dest!: reachable_extend_f)
 
 lemma (in Extend) reachable_extend_eq: 
@@ -502,17 +502,17 @@
 done
 
 lemma (in Extend) extend_Constrains:
-     "(extend h F : (extend_set h A) Co (extend_set h B)) =   
-      (F : A Co B)"
+     "(extend h F \<in> (extend_set h A) Co (extend_set h B)) =   
+      (F \<in> A Co B)"
 by (simp add: Constrains_def reachable_extend_eq extend_constrains 
               extend_set_Int_distrib [symmetric])
 
 lemma (in Extend) extend_Stable:
-     "(extend h F : Stable (extend_set h A)) = (F : Stable A)"
+     "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
 by (simp add: Stable_def extend_Constrains)
 
 lemma (in Extend) extend_Always:
-     "(extend h F : Always (extend_set h A)) = (F : Always A)"
+     "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
 by (simp (no_asm_simp) add: Always_def extend_Stable)
 
 
@@ -521,24 +521,24 @@
 (** projection: monotonicity for safety **)
 
 lemma project_act_mono:
-     "D <= C ==>  
-      project_act h (Restrict D act) <= project_act h (Restrict C act)"
+     "D \<subseteq> C ==>  
+      project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
 by (auto simp add: project_act_def)
 
 lemma (in Extend) project_constrains_mono:
-     "[| D <= C; project h C F : A co B |] ==> project h D F : A co B"
+     "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
 apply (auto simp add: constrains_def)
 apply (drule project_act_mono, blast)
 done
 
 lemma (in Extend) project_stable_mono:
-     "[| D <= C;  project h C F : stable A |] ==> project h D F : stable A"
+     "[| D \<subseteq> C;  project h C F \<in> stable A |] ==> project h D F \<in> stable A"
 by (simp add: stable_def project_constrains_mono)
 
 (*Key lemma used in several proofs about project and co*)
 lemma (in Extend) project_constrains: 
-     "(project h C F : A co B)  =   
-      (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"
+     "(project h C F \<in> A co B)  =   
+      (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)"
 apply (unfold constrains_def)
 apply (auto intro!: project_act_I simp add: ball_Un)
 apply (force intro!: project_act_I dest!: subsetD)
@@ -548,46 +548,46 @@
 done
 
 lemma (in Extend) project_stable: 
-     "(project h UNIV F : stable A) = (F : stable (extend_set h A))"
+     "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
 apply (unfold stable_def)
 apply (simp (no_asm) add: project_constrains)
 done
 
 lemma (in Extend) project_stable_I:
-     "F : stable (extend_set h A) ==> project h C F : stable A"
+     "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
 apply (drule project_stable [THEN iffD2])
 apply (blast intro: project_stable_mono)
 done
 
 lemma (in Extend) Int_extend_set_lemma:
-     "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B"
+     "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
 by (auto simp add: split_extended_all)
 
 (*Strange (look at occurrences of C) but used in leadsETo proofs*)
 lemma project_constrains_project_set:
-     "G : C co B ==> project h C G : project_set h C co project_set h B"
+     "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B"
 by (simp add: constrains_def project_def project_act_def, blast)
 
 lemma project_stable_project_set:
-     "G : stable C ==> project h C G : stable (project_set h C)"
+     "G \<in> stable C ==> project h C G \<in> stable (project_set h C)"
 by (simp add: stable_def project_constrains_project_set)
 
 
 subsection{*Progress: transient, ensures*}
 
 lemma (in Extend) extend_transient:
-     "(extend h F : transient (extend_set h A)) = (F : transient A)"
+     "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
 by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
 
 lemma (in Extend) extend_ensures:
-     "(extend h F : (extend_set h A) ensures (extend_set h B)) =  
-      (F : A ensures B)"
+     "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =  
+      (F \<in> A ensures B)"
 by (simp add: ensures_def extend_constrains extend_transient 
         extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
 
 lemma (in Extend) leadsTo_imp_extend_leadsTo:
-     "F : A leadsTo B  
-      ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"
+     "F \<in> A leadsTo B  
+      ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
 apply (erule leadsTo_induct)
   apply (simp add: leadsTo_Basis extend_ensures)
  apply (blast intro: leadsTo_Trans)
@@ -596,21 +596,21 @@
 
 subsection{*Proving the converse takes some doing!*}
 
-lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
+lemma (in Extend) slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
 by (simp (no_asm) add: slice_def)
 
-lemma (in Extend) slice_Union: "slice (Union S) y = (UN x:S. slice x y)"
+lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
 by auto
 
 lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
 by auto
 
 lemma (in Extend) project_set_is_UN_slice:
-     "project_set h A = (UN y. slice A y)"
+     "project_set h A = (\<Union>y. slice A y)"
 by auto
 
 lemma (in Extend) extend_transient_slice:
-     "extend h F : transient A ==> F : transient (slice A y)"
+     "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
 apply (unfold transient_def, auto)
 apply (rule bexI, auto)
 apply (force simp add: extend_act_def)
@@ -618,25 +618,25 @@
 
 (*Converse?*)
 lemma (in Extend) extend_constrains_slice:
-     "extend h F : A co B ==> F : (slice A y) co (slice B y)"
+     "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
 by (auto simp add: constrains_def)
 
 lemma (in Extend) extend_ensures_slice:
-     "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"
+     "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)"
 apply (auto simp add: ensures_def extend_constrains extend_transient)
 apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
 apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
 done
 
 lemma (in Extend) leadsTo_slice_project_set:
-     "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"
+     "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
 apply (simp (no_asm) add: project_set_is_UN_slice)
 apply (blast intro: leadsTo_UN)
 done
 
 lemma (in Extend) extend_leadsTo_slice [rule_format]:
-     "extend h F : AU leadsTo BU  
-      ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"
+     "extend h F \<in> AU leadsTo BU  
+      ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
 apply (erule leadsTo_induct)
   apply (blast intro: extend_ensures_slice leadsTo_Basis)
  apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
@@ -644,8 +644,8 @@
 done
 
 lemma (in Extend) extend_leadsTo:
-     "(extend h F : (extend_set h A) leadsTo (extend_set h B)) =  
-      (F : A leadsTo B)"
+     "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =  
+      (F \<in> A leadsTo B)"
 apply safe
 apply (erule_tac [2] leadsTo_imp_extend_leadsTo)
 apply (drule extend_leadsTo_slice)
@@ -653,8 +653,8 @@
 done
 
 lemma (in Extend) extend_LeadsTo:
-     "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =   
-      (F : A LeadsTo B)"
+     "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =   
+      (F \<in> A LeadsTo B)"
 by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
               extend_set_Int_distrib [symmetric])
 
@@ -662,20 +662,20 @@
 subsection{*preserves*}
 
 lemma (in Extend) project_preserves_I:
-     "G : preserves (v o f) ==> project h C G : preserves v"
+     "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
 by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
 
 (*to preserve f is to preserve the whole original state*)
 lemma (in Extend) project_preserves_id_I:
-     "G : preserves f ==> project h C G : preserves id"
+     "G \<in> preserves f ==> project h C G \<in> preserves id"
 by (simp add: project_preserves_I)
 
 lemma (in Extend) extend_preserves:
-     "(extend h G : preserves (v o f)) = (G : preserves v)"
+     "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
 by (auto simp add: preserves_def extend_stable [symmetric] 
                    extend_set_eq_Collect)
 
-lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G : preserves g)"
+lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
 by (auto simp add: preserves_def extend_def extend_act_def stable_def 
                    constrains_def g_def)
 
@@ -719,16 +719,16 @@
 done
 
 lemma (in Extend) guarantees_imp_extend_guarantees:
-     "F : X guarantees Y ==>  
-      extend h F : (extend h ` X) guarantees (extend h ` Y)"
+     "F \<in> X guarantees Y ==>  
+      extend h F \<in> (extend h ` X) guarantees (extend h ` Y)"
 apply (rule guaranteesI, clarify)
 apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D 
                    guaranteesD)
 done
 
 lemma (in Extend) extend_guarantees_imp_guarantees:
-     "extend h F : (extend h ` X) guarantees (extend h ` Y)  
-      ==> F : X guarantees Y"
+     "extend h F \<in> (extend h ` X) guarantees (extend h ` Y)  
+      ==> F \<in> X guarantees Y"
 apply (auto simp add: guar_def)
 apply (drule_tac x = "extend h G" in spec)
 apply (simp del: extend_Join 
@@ -737,8 +737,8 @@
 done
 
 lemma (in Extend) extend_guarantees_eq:
-     "(extend h F : (extend h ` X) guarantees (extend h ` Y)) =  
-      (F : X guarantees Y)"
+     "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =  
+      (F \<in> X guarantees Y)"
 by (blast intro: guarantees_imp_extend_guarantees 
                  extend_guarantees_imp_guarantees)
 
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Follows.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -12,22 +12,22 @@
 
   Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
                  (infixl "Fols" 65)
-   "f Fols g == Increasing g Int Increasing f Int
-                Always {s. f s <= g s} Int
-                (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
+   "f Fols g == Increasing g \<inter> Increasing f Int
+                Always {s. f s \<le> g s} Int
+                (\<Inter>k. {s. k \<le> g s} LeadsTo {s. k \<le> f s})"
 
 
 (*Does this hold for "invariant"?*)
 lemma mono_Always_o:
-     "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}"
+     "mono h ==> Always {s. f s \<le> g s} \<subseteq> Always {s. h (f s) \<le> h (g s)}"
 apply (simp add: Always_eq_includes_reachable)
 apply (blast intro: monoD)
 done
 
 lemma mono_LeadsTo_o:
      "mono (h::'a::order => 'b::order)  
-      ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <=  
-          (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})"
+      ==> (\<Inter>j. {s. j \<le> g s} LeadsTo {s. j \<le> f s}) \<subseteq>  
+          (\<Inter>k. {s. k \<le> h (g s)} LeadsTo {s. k \<le> h (f s)})"
 apply auto
 apply (rule single_LeadsTo_I)
 apply (drule_tac x = "g s" in spec)
@@ -35,10 +35,10 @@
 apply (blast intro: monoD order_trans)+
 done
 
-lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)"
+lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)"
 by (unfold Follows_def, auto)
 
-lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)"
+lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)"
 apply (unfold Follows_def, clarify)
 apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD]
                  mono_Always_o [THEN [2] rev_subsetD]
@@ -46,13 +46,13 @@
 done
 
 lemma mono_Follows_apply:
-     "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))"
+     "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))"
 apply (drule mono_Follows_o)
 apply (force simp add: o_def)
 done
 
 lemma Follows_trans: 
-     "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h"
+     "[| F \<in> f Fols g;  F \<in> g Fols h |] ==> F \<in> f Fols h"
 apply (unfold Follows_def)
 apply (simp add: Always_eq_includes_reachable)
 apply (blast intro: order_trans LeadsTo_Trans)
@@ -61,24 +61,24 @@
 
 subsection{*Destruction rules*}
 
-lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f"
+lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
 apply (unfold Follows_def, blast)
 done
 
-lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g"
+lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
 apply (unfold Follows_def, blast)
 done
 
-lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}"
+lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
 apply (unfold Follows_def, blast)
 done
 
 lemma Follows_LeadsTo: 
-     "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"
+     "F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
 by (unfold Follows_def, blast)
 
 lemma Follows_LeadsTo_pfixLe:
-     "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
+     "F \<in> f Fols g ==> F \<in> {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
 apply (rule single_LeadsTo_I, clarify)
 apply (drule_tac k="g s" in Follows_LeadsTo)
 apply (erule LeadsTo_weaken)
@@ -87,7 +87,7 @@
 done
 
 lemma Follows_LeadsTo_pfixGe:
-     "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
+     "F \<in> f Fols g ==> F \<in> {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
 apply (rule single_LeadsTo_I, clarify)
 apply (drule_tac k="g s" in Follows_LeadsTo)
 apply (erule LeadsTo_weaken)
@@ -97,21 +97,21 @@
 
 
 lemma Always_Follows1: 
-     "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"
+     "[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g"
 
 apply (unfold Follows_def Increasing_def Stable_def, auto)
 apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}" 
+apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}" 
        in Always_Constrains_weaken, auto)
 apply (drule Always_Int_I, assumption)
 apply (force intro: Always_weaken)
 done
 
 lemma Always_Follows2: 
-     "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"
+     "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
 apply (unfold Follows_def Increasing_def Stable_def, auto)
 apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}"
+apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
        in Always_Constrains_weaken, auto)
 apply (drule Always_Int_I, assumption)
 apply (force intro: Always_weaken)
@@ -122,8 +122,8 @@
 
 (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
 lemma increasing_Un: 
-    "[| F : increasing f;  F: increasing g |]  
-     ==> F : increasing (%s. (f s) Un (g s))"
+    "[| F \<in> increasing f;  F \<in> increasing g |]  
+     ==> F \<in> increasing (%s. (f s) \<union> (g s))"
 apply (unfold increasing_def stable_def constrains_def, auto)
 apply (drule_tac x = "f xa" in spec)
 apply (drule_tac x = "g xa" in spec)
@@ -131,8 +131,8 @@
 done
 
 lemma Increasing_Un: 
-    "[| F : Increasing f;  F: Increasing g |]  
-     ==> F : Increasing (%s. (f s) Un (g s))"
+    "[| F \<in> Increasing f;  F \<in> Increasing g |]  
+     ==> F \<in> Increasing (%s. (f s) \<union> (g s))"
 apply (auto simp add: Increasing_def Stable_def Constrains_def
                       stable_def constrains_def)
 apply (drule_tac x = "f xa" in spec)
@@ -142,17 +142,17 @@
 
 
 lemma Always_Un:
-     "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]  
-      ==> F : Always {s. f' s Un g' s <= f s Un g s}"
+     "[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]  
+      ==> F \<in> Always {s. f' s \<union> g' s \<le> f s \<union> g s}"
 by (simp add: Always_eq_includes_reachable, blast)
 
 (*Lemma to re-use the argument that one variable increases (progress)
   while the other variable doesn't decrease (safety)*)
 lemma Follows_Un_lemma:
-     "[| F : Increasing f; F : Increasing g;  
-         F : Increasing g'; F : Always {s. f' s <= f s}; 
-         ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |] 
-      ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}"
+     "[| F \<in> Increasing f; F \<in> Increasing g;  
+         F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s}; 
+         \<forall>k. F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |] 
+      ==> F \<in> {s. k \<le> f s \<union> g s} LeadsTo {s. k \<le> f' s \<union> g s}"
 apply (rule single_LeadsTo_I)
 apply (drule_tac x = "f s" in IncreasingD)
 apply (drule_tac x = "g s" in IncreasingD)
@@ -164,8 +164,8 @@
 done
 
 lemma Follows_Un: 
-    "[| F : f' Fols f;  F: g' Fols g |]  
-     ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))"
+    "[| F \<in> f' Fols f;  F \<in> g' Fols g |]  
+     ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
 apply (unfold Follows_def)
 apply (simp add: Increasing_Un Always_Un, auto)
 apply (rule LeadsTo_Trans)
@@ -178,8 +178,8 @@
 subsection{*Multiset union properties (with the multiset ordering)*}
 
 lemma increasing_union: 
-    "[| F : increasing f;  F: increasing g |]  
-     ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+    "[| F \<in> increasing f;  F \<in> increasing g |]  
+     ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
 apply (unfold increasing_def stable_def constrains_def, auto)
 apply (drule_tac x = "f xa" in spec)
 apply (drule_tac x = "g xa" in spec)
@@ -188,8 +188,8 @@
 done
 
 lemma Increasing_union: 
-    "[| F : Increasing f;  F: Increasing g |]  
-     ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+    "[| F \<in> Increasing f;  F \<in> Increasing g |]  
+     ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
 apply (auto simp add: Increasing_def Stable_def Constrains_def
                       stable_def constrains_def)
 apply (drule_tac x = "f xa" in spec)
@@ -199,19 +199,19 @@
 done
 
 lemma Always_union:
-     "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]  
-      ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}"
+     "[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]  
+      ==> F \<in> Always {s. f' s + g' s \<le> f s + (g s :: ('a::order) multiset)}"
 apply (simp add: Always_eq_includes_reachable)
 apply (blast intro: union_le_mono)
 done
 
 (*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
 lemma Follows_union_lemma:
-     "[| F : Increasing f; F : Increasing g;  
-         F : Increasing g'; F : Always {s. f' s <= f s}; 
-         ALL k::('a::order) multiset.  
-           F : {s. k <= f s} LeadsTo {s. k <= f' s} |] 
-      ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}"
+     "[| F \<in> Increasing f; F \<in> Increasing g;  
+         F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s}; 
+         \<forall>k::('a::order) multiset.  
+           F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |] 
+      ==> F \<in> {s. k \<le> f s + g s} LeadsTo {s. k \<le> f' s + g s}"
 apply (rule single_LeadsTo_I)
 apply (drule_tac x = "f s" in IncreasingD)
 apply (drule_tac x = "g s" in IncreasingD)
@@ -226,8 +226,8 @@
 (*The !! is there to influence to effect of permutative rewriting at the end*)
 lemma Follows_union: 
      "!!g g' ::'b => ('a::order) multiset.  
-        [| F : f' Fols f;  F: g' Fols g |]  
-        ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
+        [| F \<in> f' Fols f;  F \<in> g' Fols g |]  
+        ==> F \<in> (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
 apply (unfold Follows_def)
 apply (simp add: Increasing_union Always_union, auto)
 apply (rule LeadsTo_Trans)
@@ -239,8 +239,8 @@
 
 lemma Follows_setsum:
      "!!f ::['c,'b] => ('a::order) multiset.  
-        [| ALL i: I. F : f' i Fols f i;  finite I |]  
-        ==> F : (%s. \<Sum>i:I. f' i s) Fols (%s. \<Sum>i:I. f i s)"
+        [| \<forall>i \<in> I. F \<in> f' i Fols f i;  finite I |]  
+        ==> F \<in> (%s. \<Sum>i \<in> I. f' i s) Fols (%s. \<Sum>i \<in> I. f i s)"
 apply (erule rev_mp)
 apply (erule finite_induct, simp) 
 apply (simp add: Follows_union)
@@ -249,7 +249,7 @@
 
 (*Currently UNUSED, but possibly of interest*)
 lemma Increasing_imp_Stable_pfixGe:
-     "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}"
+     "F \<in> Increasing func ==> F \<in> Stable {s. h pfixGe (func s)}"
 apply (simp add: Increasing_def Stable_def Constrains_def constrains_def)
 apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] 
                     prefix_imp_pfixGe)
@@ -257,8 +257,8 @@
 
 (*Currently UNUSED, but possibly of interest*)
 lemma LeadsTo_le_imp_pfixGe:
-     "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s}  
-      ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
+     "\<forall>z. F \<in> {s. z \<le> f s} LeadsTo {s. z \<le> g s}  
+      ==> F \<in> {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
 apply (rule single_LeadsTo_I)
 apply (drule_tac x = "f s" in spec)
 apply (erule LeadsTo_weaken)
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -32,57 +32,57 @@
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
   ex_prop  :: "'a program set => bool"
-   "ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X"
+   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
 
   strict_ex_prop  :: "'a program set => bool"
-   "strict_ex_prop X == \<forall>F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
+   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
 
   uv_prop  :: "'a program set => bool"
-   "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
+   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
 
   strict_uv_prop  :: "'a program set => bool"
    "strict_uv_prop X == 
-      SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
+      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
 
   guar :: "['a program set, 'a program set] => 'a program set"
           (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
-   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}"
+   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
   
 
   (* Weakest guarantees *)
    wg :: "['a program, 'a program set] =>  'a program set"
-  "wg F Y == Union({X. F:X guarantees Y})"
+  "wg F Y == Union({X. F \<in> X guarantees Y})"
 
    (* Weakest existential property stronger than X *)
    wx :: "('a program) set => ('a program)set"
-   "wx X == Union({Y. Y<=X & ex_prop Y})"
+   "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
   
   (*Ill-defined programs can arise through "Join"*)
   welldef :: "'a program set"
-  "welldef == {F. Init F ~= {}}"
+  "welldef == {F. Init F \<noteq> {}}"
   
   refines :: "['a program, 'a program, 'a program set] => bool"
 			("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
-     \<forall>H. (F ok H  & G ok H & F Join H : welldef Int X) --> 
-         (G Join H : welldef Int X)"
+     \<forall>H. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X) --> 
+         (G Join H \<in> welldef \<inter> X)"
 
   iso_refines :: "['a program, 'a program, 'a program set] => bool"
                               ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
   "G iso_refines F wrt X ==
-   F : welldef Int X --> G : welldef Int X"
+   F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
 
 
 lemma OK_insert_iff:
      "(OK (insert i I) F) = 
-      (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
+      (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
 by (auto intro: ok_sym simp add: OK_iff_ok)
 
 
 (*** existential properties ***)
 lemma ex1 [rule_format]: 
  "[| ex_prop X; finite GG |] ==>  
-     GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
+     GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
 apply (unfold ex_prop_def)
 apply (erule finite_induct)
 apply (auto simp add: OK_insert_iff Int_insert_left)
@@ -90,7 +90,7 @@
 
 
 lemma ex2: 
-     "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X 
+     "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X 
       ==> ex_prop X"
 apply (unfold ex_prop_def, clarify)
 apply (drule_tac x = "{F,G}" in spec)
@@ -101,13 +101,13 @@
 (*Chandy & Sanders take this as a definition*)
 lemma ex_prop_finite:
      "ex_prop X = 
-      (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
+      (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
 by (blast intro: ex1 ex2)
 
 
 (*Their "equivalent definition" given at the end of section 3*)
 lemma ex_prop_equiv: 
-     "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
+     "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
 apply auto
 apply (unfold ex_prop_def component_of_def, safe)
 apply blast 
@@ -120,14 +120,14 @@
 (*** universal properties ***)
 lemma uv1 [rule_format]: 
      "[| uv_prop X; finite GG |] 
-      ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
+      ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
 apply (unfold uv_prop_def)
 apply (erule finite_induct)
 apply (auto simp add: Int_insert_left OK_insert_iff)
 done
 
 lemma uv2: 
-     "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X  
+     "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
       ==> uv_prop X"
 apply (unfold uv_prop_def)
 apply (rule conjI)
@@ -141,37 +141,37 @@
 (*Chandy & Sanders take this as a definition*)
 lemma uv_prop_finite:
      "uv_prop X = 
-      (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
+      (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
 by (blast intro: uv1 uv2)
 
 (*** guarantees ***)
 
 lemma guaranteesI:
-     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)  
-      ==> F : X guarantees Y"
+     "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)  
+      ==> F \<in> X guarantees Y"
 by (simp add: guar_def component_def)
 
 lemma guaranteesD: 
-     "[| F : X guarantees Y;  F ok G;  F Join G : X |]  
-      ==> F Join G : Y"
+     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X |]  
+      ==> F Join G \<in> Y"
 by (unfold guar_def component_def, blast)
 
 (*This version of guaranteesD matches more easily in the conclusion
-  The major premise can no longer be  F<=H since we need to reason about G*)
+  The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
 lemma component_guaranteesD: 
-     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |]  
-      ==> H : Y"
+     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G |]  
+      ==> H \<in> Y"
 by (unfold guar_def, blast)
 
 lemma guarantees_weaken: 
-     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
+     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
 by (unfold guar_def, blast)
 
-lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
+lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
 by (unfold guar_def, blast)
 
 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
+lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
 by (unfold guar_def, blast)
 
 (*Remark at end of section 4.1 *)
@@ -201,31 +201,31 @@
 (** Distributive laws.  Re-orient to perform miniscoping **)
 
 lemma guarantees_UN_left: 
-     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
+     "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
 by (unfold guar_def, blast)
 
 lemma guarantees_Un_left: 
-     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
+     "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
 by (unfold guar_def, blast)
 
 lemma guarantees_INT_right: 
-     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
+     "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
 by (unfold guar_def, blast)
 
 lemma guarantees_Int_right: 
-     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
+     "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
 by (unfold guar_def, blast)
 
 lemma guarantees_Int_right_I:
-     "[| F : Z guarantees X;  F : Z guarantees Y |]  
-     ==> F : Z guarantees (X Int Y)"
+     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
+     ==> F \<in> Z guarantees (X \<inter> Y)"
 by (simp add: guarantees_Int_right)
 
 lemma guarantees_INT_right_iff:
-     "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
+     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
 by (simp add: guarantees_INT_right)
 
-lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
+lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
 by (unfold guar_def, blast)
 
 lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
@@ -236,35 +236,35 @@
 **)
 
 lemma combining1: 
-    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |] 
-     ==> F : (V Int Y) guarantees Z"
+    "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
+     ==> F \<in> (V \<inter> Y) guarantees Z"
 
 by (unfold guar_def, blast)
 
 lemma combining2: 
-    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |] 
-     ==> F : V guarantees (X Un Z)"
+    "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
+     ==> F \<in> V guarantees (X \<union> Z)"
 by (unfold guar_def, blast)
 
 (** The following two follow Chandy-Sanders, but the use of object-quantifiers
     does not suit Isabelle... **)
 
-(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
 lemma all_guarantees: 
-     "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
+     "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
 by (unfold guar_def, blast)
 
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
 lemma ex_guarantees: 
-     "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
+     "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
 by (unfold guar_def, blast)
 
 
 (*** Additional guarantees laws, by lcp ***)
 
 lemma guarantees_Join_Int: 
-    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]  
-     ==> F Join G: (U Int X) guarantees (V Int Y)"
+    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
+     ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
@@ -275,8 +275,8 @@
 done
 
 lemma guarantees_Join_Un: 
-    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]   
-     ==> F Join G: (U Un X) guarantees (V Un Y)"
+    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
+     ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
@@ -287,8 +287,8 @@
 done
 
 lemma guarantees_JN_INT: 
-     "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]  
-      ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
+     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
+      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
@@ -298,8 +298,8 @@
 done
 
 lemma guarantees_JN_UN: 
-    "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]  
-     ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
+    "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
+     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
@@ -312,7 +312,7 @@
 (*** guarantees laws for breaking down the program, by lcp ***)
 
 lemma guarantees_Join_I1: 
-     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
+     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
@@ -320,14 +320,14 @@
 done
 
 lemma guarantees_Join_I2:
-     "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
+     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
 apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
 apply (blast intro: guarantees_Join_I1)
 done
 
 lemma guarantees_JN_I: 
-     "[| i : I;  F i: X guarantees Y;  OK I F |]  
-      ==> (JN i:I. (F i)) : X guarantees Y"
+     "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
+      ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
 apply (unfold guar_def, clarify)
 apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
 apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
@@ -336,10 +336,10 @@
 
 (*** well-definedness ***)
 
-lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
+lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
 by (unfold welldef_def, auto)
 
-lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
+lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
 by (unfold welldef_def, auto)
 
 (*** refinement ***)
@@ -357,14 +357,14 @@
 
 lemma strict_ex_refine_lemma: 
      "strict_ex_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)  
-              = (F:X --> G:X)"
+      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)  
+              = (F \<in> X --> G \<in> X)"
 by (unfold strict_ex_prop_def, auto)
 
 lemma strict_ex_refine_lemma_v: 
      "strict_ex_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =  
-          (F: welldef Int X --> G:X)"
+      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
+          (F \<in> welldef \<inter> X --> G \<in> X)"
 apply (unfold strict_ex_prop_def, safe)
 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -372,7 +372,7 @@
 
 lemma ex_refinement_thm:
      "[| strict_ex_prop X;   
-         \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]  
+         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]  
       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
 apply (rule_tac x = SKIP in allE, assumption)
 apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
@@ -381,13 +381,13 @@
 
 lemma strict_uv_refine_lemma: 
      "strict_uv_prop X ==> 
-      (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"
+      (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
 by (unfold strict_uv_prop_def, blast)
 
 lemma strict_uv_refine_lemma_v: 
      "strict_uv_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =  
-          (F: welldef Int X --> G:X)"
+      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
+          (F \<in> welldef \<inter> X --> G \<in> X)"
 apply (unfold strict_uv_prop_def, safe)
 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -395,8 +395,8 @@
 
 lemma uv_refinement_thm:
      "[| strict_uv_prop X;   
-         \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> 
-             G Join H : welldef |]  
+         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> 
+             G Join H \<in> welldef |]  
       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
 apply (rule_tac x = SKIP in allE, assumption)
 apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
@@ -404,17 +404,17 @@
 
 (* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
 lemma guarantees_equiv: 
-    "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
+    "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
 by (unfold guar_def component_of_def, auto)
 
-lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
+lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
 by (unfold wg_def, auto)
 
 lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
 by (unfold wg_def guar_def, blast)
 
 lemma wg_equiv: 
-  "(H: wg F X) = (F component_of H --> H:X)"
+  "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
 apply (unfold wg_def)
 apply (simp (no_asm) add: guarantees_equiv)
 apply (rule iffI)
@@ -423,21 +423,21 @@
 done
 
 
-lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
+lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
 by (simp add: wg_equiv)
 
 lemma wg_finite: 
-    "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)  
-          --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
+    "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)  
+          --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
 apply clarify
-apply (subgoal_tac "F component_of (JN F:FF. F) ")
+apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
 apply (drule_tac X = X in component_of_wg, simp)
 apply (simp add: component_of_def)
-apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
+apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
 apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
 done
 
-lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
+lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
 apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
 apply blast
 done
@@ -455,11 +455,11 @@
 apply auto
 done
 
-lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
+lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
 by (unfold wx_def, auto)
 
 (* Proposition 6 *)
-lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
 apply (unfold ex_prop_def, safe)
 apply (drule_tac x = "G Join Ga" in spec)
 apply (force simp add: ok_Join_iff1 Join_assoc)
@@ -483,7 +483,7 @@
 apply (drule_tac x = G in spec)
 apply (frule_tac c = "x Join G" in subsetD, safe)
 apply (simp (no_asm))
-apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
 apply (rule_tac [2] wx'_ex_prop)
 apply (rotate_tac 1)
 apply (drule_tac x = SKIP in spec, auto)
@@ -496,7 +496,7 @@
 (* Proposition 12 *)
 (* Main result of the paper *)
 lemma guarantees_wx_eq: 
-   "(X guarantees Y) = wx(-X Un Y)"
+   "(X guarantees Y) = wx(-X \<union> Y)"
 apply (unfold guar_def)
 apply (simp (no_asm) add: wx_equiv)
 done
@@ -511,7 +511,7 @@
     Reasoning About Program composition paper *)
 
 lemma stable_guarantees_Always:
-     "Init F <= A ==> F:(stable A) guarantees (Always A)"
+     "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
 apply (rule guaranteesI)
 apply (simp (no_asm) add: Join_commute)
 apply (rule stable_Join_Always1)
@@ -519,7 +519,7 @@
 done
 
 (* To be moved to WFair.ML *)
-lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
+lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
 apply (drule_tac B = "A-B" in constrains_weaken_L)
 apply (drule_tac [2] B = "A-B" in transient_strengthen)
 apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
@@ -529,7 +529,7 @@
 
 
 lemma constrains_guarantees_leadsTo:
-     "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
+     "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
 apply (rule guaranteesI)
 apply (rule leadsTo_Basis')
 apply (drule constrains_weaken_R)
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -116,23 +116,23 @@
 lemma lift_set_empty [simp]: "lift_set i {} = {}"
 by (unfold lift_set_def, auto)
 
-lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)"
+lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)"
 apply (unfold lift_set_def)
 apply (rule inj_lift_map [THEN inj_image_mem_iff])
 done
 
 (*Do we really need both this one and its predecessor?*)
 lemma lift_set_iff2 [iff]:
-     "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
+     "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)"
 by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
 
 
-lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
+lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B"
 apply (unfold lift_set_def)
 apply (erule image_mono)
 done
 
-lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
+lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
 apply (unfold lift_set_def)
 apply (simp add: image_Un)
 done
@@ -154,39 +154,39 @@
 lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
 by (simp add: lift_def)
 
-lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
+lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
 by (simp add: lift_def)
 
 (*** Safety: co, stable, invariant ***)
 
 lemma lift_constrains: 
-     "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
+     "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
 by (simp add: lift_def lift_set_def rename_constrains)
 
 lemma lift_stable: 
-     "(lift i F : stable (lift_set i A)) = (F : stable A)"
+     "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)"
 by (simp add: lift_def lift_set_def rename_stable)
 
 lemma lift_invariant: 
-     "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
+     "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_invariant)
 done
 
 lemma lift_Constrains: 
-     "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
+     "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Constrains)
 done
 
 lemma lift_Stable: 
-     "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
+     "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Stable)
 done
 
 lemma lift_Always: 
-     "(lift i F : Always (lift_set i A)) = (F : Always A)"
+     "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
 apply (unfold lift_def lift_set_def)
 apply (simp add: rename_Always)
 done
@@ -194,37 +194,37 @@
 (*** Progress: transient, ensures ***)
 
 lemma lift_transient: 
-     "(lift i F : transient (lift_set i A)) = (F : transient A)"
+     "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
 by (simp add: lift_def lift_set_def rename_transient)
 
 lemma lift_ensures: 
-     "(lift i F : (lift_set i A) ensures (lift_set i B)) =  
-      (F : A ensures B)"
+     "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) =  
+      (F \<in> A ensures B)"
 by (simp add: lift_def lift_set_def rename_ensures)
 
 lemma lift_leadsTo: 
-     "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =  
-      (F : A leadsTo B)"
+     "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) =  
+      (F \<in> A leadsTo B)"
 by (simp add: lift_def lift_set_def rename_leadsTo)
 
 lemma lift_LeadsTo: 
-     "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =   
-      (F : A LeadsTo B)"
+     "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) =   
+      (F \<in> A LeadsTo B)"
 by (simp add: lift_def lift_set_def rename_LeadsTo)
 
 
 (** guarantees **)
 
 lemma lift_lift_guarantees_eq: 
-     "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =  
-      (F : X guarantees Y)"
+     "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) =  
+      (F \<in> X guarantees Y)"
 apply (unfold lift_def)
 apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
 apply (simp add: o_def)
 done
 
-lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =  
-      (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
+lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =  
+      (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
 by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
 
 
@@ -236,14 +236,14 @@
 (*To preserve snd means that the second component is there just to allow
   guarantees properties to be stated.  Converse fails, for lift i F can 
   change function components other than i*)
-lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
+lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
 apply (simp add: lift_def rename_preserves)
 apply (simp add: lift_map_def o_def split_def)
 done
 
 lemma delete_map_eqE':
-     "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
+     "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)"
 apply (drule_tac f = "insert_map i (g i) " in arg_cong)
 apply (simp add: insert_map_delete_map_eq)
 apply (erule exI)
@@ -252,7 +252,7 @@
 lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
 
 lemma delete_map_neq_apply:
-     "[| delete_map j g = delete_map j g';  i~=j |] ==> g i = g' i"
+     "[| delete_map j g = delete_map j g';  i\<noteq>j |] ==> g i = g' i"
 by force
 
 (*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
@@ -265,27 +265,27 @@
 by auto
 
 lemma mem_lift_act_iff [iff]: 
-     "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) =  
-      ((drop_map i s, drop_map i s') : act)"
+     "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) =  
+      ((drop_map i s, drop_map i s') \<in> act)"
 apply (unfold extend_act_def, auto)
 apply (rule bexI, auto)
 done
 
 lemma preserves_snd_lift_stable:
-     "[| F : preserves snd;  i~=j |]  
-      ==> lift j F : stable (lift_set i (A <*> UNIV))"
+     "[| F \<in> preserves snd;  i\<noteq>j |]  
+      ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
 apply (auto simp add: lift_def lift_set_def stable_def constrains_def 
                       rename_def extend_def mem_rename_set_iff)
 apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
 apply (drule_tac x = i in fun_cong, auto)
 done
 
-(*If i~=j then lift j F  does nothing to lift_set i, and the 
-  premise ensures A<=B.*)
+(*If i\<noteq>j then lift j F  does nothing to lift_set i, and the 
+  premise ensures A \<subseteq> B.*)
 lemma constrains_imp_lift_constrains:
-    "[| F i : (A <*> UNIV) co (B <*> UNIV);   
-        F j : preserves snd |]   
-     ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+    "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
+        F j \<in> preserves snd |]   
+     ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
 apply (case_tac "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
@@ -309,24 +309,24 @@
 done
 
 lemma insert_map_eq_diff:
-     "[| insert_map i s f = insert_map j t g;  i~=j |]  
-      ==> EX g'. insert_map i s' f = insert_map j t g'"
+     "[| insert_map i s f = insert_map j t g;  i\<noteq>j |]  
+      ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
 apply (subst insert_map_upd_same [symmetric])
 apply (erule ssubst)
 apply (simp only: insert_map_upd if_False split: split_if, blast)
 done
 
 lemma lift_map_eq_diff: 
-     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i~=j |]  
-      ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
+     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i\<noteq>j |]  
+      ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
 apply (unfold lift_map_def, auto)
 apply (blast dest: insert_map_eq_diff)
 done
 
 lemma lift_transient_eq_disj:
-     "F : preserves snd  
-      ==> (lift i F : transient (lift_set j (A <*> UNIV))) =  
-          (i=j & F : transient (A <*> UNIV) | A={})"
+     "F \<in> preserves snd  
+      ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =  
+          (i=j & F \<in> transient (A <*> UNIV) | A={})"
 apply (case_tac "i=j")
 apply (auto simp add: lift_transient)
 apply (auto simp add: lift_set_def lift_def transient_def rename_def 
@@ -346,21 +346,21 @@
 
 (*USELESS??*)
 lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =  
-      (UN s:A. UN f. {insert_map i s f}) <*> UNIV"
+      (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
 apply (auto intro!: bexI image_eqI simp add: lift_map_def)
 apply (rule split_conv [symmetric])
 done
 
 lemma lift_preserves_eq:
-     "(lift i F : preserves v) = (F : preserves (v o lift_map i))"
+     "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))"
 by (simp add: lift_def rename_preserves)
 
 (*A useful rewrite.  If o, sub have been rewritten out already then can also
   use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
 lemma lift_preserves_sub:
-     "F : preserves snd  
-      ==> lift i F : preserves (v o sub j o fst) =  
-          (if i=j then F : preserves (v o fst) else True)"
+     "F \<in> preserves snd  
+      ==> lift i F \<in> preserves (v o sub j o fst) =  
+          (if i=j then F \<in> preserves (v o fst) else True)"
 apply (drule subset_preserves_o [THEN subsetD])
 apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
 apply (auto cong del: if_weak_cong 
@@ -374,7 +374,7 @@
 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
 by (simp add: expand_fun_eq o_def)
 
-lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x"
+lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
 by (simp add: expand_fun_eq o_def)
 
 lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
@@ -402,7 +402,7 @@
 
 lemma project_act_extend_act:
      "project_act h (extend_act h' act) =  
-        {(x,x'). EX s s' y y' z. (s,s') : act &  
+        {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act &  
                  h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
 by (simp add: extend_act_def project_act_def, blast)
 
@@ -410,24 +410,24 @@
 (*** OK and "lift" ***)
 
 lemma act_in_UNION_preserves_fst:
-     "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"
+     "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
 apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
 apply (auto simp add: preserves_def stable_def constrains_def)
 done
 
 lemma UNION_OK_lift_I:
-     "[| ALL i:I. F i : preserves snd;   
-         ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]  
+     "[| \<forall>i \<in> I. F i \<in> preserves snd;   
+         \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]  
       ==> OK I (%i. lift i (F i))"
 apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
 apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
 apply (rename_tac "act")
 apply (subgoal_tac
        "{(x, x'). \<exists>s f u s' f' u'. 
-                    ((s, f, u), s', f', u') : act & 
+                    ((s, f, u), s', f', u') \<in> act & 
                     lift_map j x = lift_map i (s, f, u) & 
                     lift_map j x' = lift_map i (s', f', u') } 
-                <= { (x,x') . fst x = fst x'}")
+                \<subseteq> { (x,x') . fst x = fst x'}")
 apply (blast intro: act_in_UNION_preserves_fst, clarify)
 apply (drule_tac x = j in fun_cong)+
 apply (drule_tac x = i in bspec, assumption)
@@ -435,8 +435,8 @@
 done
 
 lemma OK_lift_I:
-     "[| ALL i:I. F i : preserves snd;   
-         ALL i:I. preserves fst <= Allowed (F i) |]  
+     "[| \<forall>i \<in> I. F i \<in> preserves snd;   
+         \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |]  
       ==> OK I (%i. lift i (F i))"
 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
 
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -15,19 +15,19 @@
 
   PLam  :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
             => ((nat=>'b) * 'c) program"
-    "PLam I F == JN i:I. lift i (F i)"
+    "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
 
 syntax
   "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
               ("(3plam _:_./ _)" 10)
 
 translations
-  "plam x:A. B"   == "PLam A (%x. B)"
+  "plam x : A. B"   == "PLam A (%x. B)"
 
 
 (*** Basic properties ***)
 
-lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"
+lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
 apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
 done
 
@@ -37,7 +37,7 @@
 apply (simp (no_asm) add: PLam_def)
 done
 
-lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP"
+lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP"
 apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
 done
 
@@ -46,11 +46,11 @@
 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
 by (unfold PLam_def, auto)
 
-lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"
+lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
 apply (simp (no_asm) add: PLam_def JN_component_iff)
 done
 
-lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)"
+lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
 apply (unfold PLam_def)
 (*blast_tac doesn't use HO unification*)
 apply (fast intro: component_JN)
@@ -60,10 +60,10 @@
 (** Safety & Progress: but are they used anywhere? **)
 
 lemma PLam_constrains: 
-     "[| i : I;  ALL j. F j : preserves snd |] ==>   
-      (PLam I F : (lift_set i (A <*> UNIV)) co  
+     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |] ==>   
+      (PLam I F \<in> (lift_set i (A <*> UNIV)) co  
                   (lift_set i (B <*> UNIV)))  =   
-      (F i : (A <*> UNIV) co (B <*> UNIV))"
+      (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
 apply (simp (no_asm_simp) add: PLam_def JN_constrains)
 apply (subst insert_Diff [symmetric], assumption)
 apply (simp (no_asm_simp) add: lift_constrains)
@@ -71,33 +71,33 @@
 done
 
 lemma PLam_stable: 
-     "[| i : I;  ALL j. F j : preserves snd |]   
-      ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =  
-          (F i : stable (A <*> UNIV))"
+     "[| i \<in> I;  \<forall>j. F j \<in> preserves snd |]   
+      ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =  
+          (F i \<in> stable (A <*> UNIV))"
 apply (simp (no_asm_simp) add: stable_def PLam_constrains)
 done
 
 lemma PLam_transient: 
-     "i : I ==>  
-    PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
+     "i \<in> I ==>  
+    PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
 apply (simp (no_asm_simp) add: JN_transient PLam_def)
 done
 
 (*This holds because the F j cannot change (lift_set i)*)
 lemma PLam_ensures: 
-     "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);   
-         ALL j. F j : preserves snd |] ==>   
-      PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+     "[| i \<in> I;  F i \<in> (A <*> UNIV) ensures (B <*> UNIV);   
+         \<forall>j. F j \<in> preserves snd |] ==>   
+      PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
 apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
 done
 
 lemma PLam_leadsTo_Basis: 
-     "[| i : I;   
-         F i : ((A <*> UNIV) - (B <*> UNIV)) co  
-               ((A <*> UNIV) Un (B <*> UNIV));   
-         F i : transient ((A <*> UNIV) - (B <*> UNIV));   
-         ALL j. F j : preserves snd |] ==>   
-      PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+     "[| i \<in> I;   
+         F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co  
+               ((A <*> UNIV) \<union> (B <*> UNIV));   
+         F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));   
+         \<forall>j. F j \<in> preserves snd |] ==>   
+      PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
 by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
 
 
@@ -105,20 +105,20 @@
 (** invariant **)
 
 lemma invariant_imp_PLam_invariant: 
-     "[| F i : invariant (A <*> UNIV);  i : I;   
-         ALL j. F j : preserves snd |]  
-      ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
+     "[| F i \<in> invariant (A <*> UNIV);  i \<in> I;   
+         \<forall>j. F j \<in> preserves snd |]  
+      ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
 by (auto simp add: PLam_stable invariant_def)
 
 
 lemma PLam_preserves_fst [simp]:
-     "ALL j. F j : preserves snd  
-      ==> (PLam I F : preserves (v o sub j o fst)) =  
-          (if j: I then F j : preserves (v o fst) else True)"
+     "\<forall>j. F j \<in> preserves snd  
+      ==> (PLam I F \<in> preserves (v o sub j o fst)) =  
+          (if j \<in> I then F j \<in> preserves (v o fst) else True)"
 by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
 
 lemma PLam_preserves_snd [simp,intro]:
-     "ALL j. F j : preserves snd ==> PLam I F : preserves snd"
+     "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
 by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
 
 
@@ -130,44 +130,44 @@
   something like lift_preserves_sub to rewrite the third.  However there's
   no obvious way to alternative for the third premise.*)
 lemma guarantees_PLam_I: 
-    "[| lift i (F i): X guarantees Y;  i : I;   
+    "[| lift i (F i): X guarantees Y;  i \<in> I;   
         OK I (%i. lift i (F i)) |]   
-     ==> (PLam I F) : X guarantees Y"
+     ==> (PLam I F) \<in> X guarantees Y"
 apply (unfold PLam_def)
 apply (simp (no_asm_simp) add: guarantees_JN_I)
 done
 
 lemma Allowed_PLam [simp]:
-     "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"
+     "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
 by (simp (no_asm) add: PLam_def)
 
 
 lemma PLam_preserves [simp]:
-     "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"
-by (simp (no_asm) add: PLam_def lift_def rename_preserves)
+     "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
+by (simp add: PLam_def lift_def rename_preserves)
 
 
 (**UNUSED
     (*The f0 premise ensures that the product is well-defined.*)
     lemma PLam_invariant_imp_invariant: 
-     "[| PLam I F : invariant (lift_set i A);  i : I;   
-             f0: Init (PLam I F) |] ==> F i : invariant A"
+     "[| PLam I F \<in> invariant (lift_set i A);  i \<in> I;   
+             f0: Init (PLam I F) |] ==> F i \<in> invariant A"
     apply (auto simp add: invariant_def)
     apply (drule_tac c = "f0 (i:=x) " in subsetD)
     apply auto
     done
 
     lemma PLam_invariant: 
-     "[| i : I;  f0: Init (PLam I F) |]  
-          ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
+     "[| i \<in> I;  f0: Init (PLam I F) |]  
+          ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
     apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
     done
 
     (*The f0 premise isn't needed if F is a constant program because then
       we get an initial state by replicating that of F*)
     lemma reachable_PLam: 
-     "i : I  
-          ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
+     "i \<in> I  
+          ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
     apply (auto simp add: invariant_def)
     done
 **)
@@ -176,25 +176,25 @@
 (**UNUSED
     (** Reachability **)
 
-    Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)"
+    Goal "[| f \<in> reachable (PLam I F);  i \<in> I |] ==> f i \<in> reachable (F i)"
     apply (erule reachable.induct)
     apply (auto intro: reachable.intrs)
     done
 
     (*Result to justify a re-organization of this file*)
-    lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
+    lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
     by auto
 
     lemma reachable_PLam_subset1: 
-     "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
+     "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
     apply (force dest!: reachable_PLam)
     done
 
     (*simplify using reachable_lift??*)
     lemma reachable_lift_Join_PLam [rule_format]:
-      "[| i ~: I;  A : reachable (F i) |]      
-       ==> ALL f. f : reachable (PLam I F)       
-                  --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
+      "[| i \<notin> I;  A \<in> reachable (F i) |]      
+       ==> \<forall>f. f \<in> reachable (PLam I F)       
+                  --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
     apply (erule reachable.induct)
     apply (ALLGOALS Clarify_tac)
     apply (erule reachable.induct)
@@ -224,7 +224,7 @@
       perform actions, and PLam can never catch up in finite time.*)
     lemma reachable_PLam_subset2: 
      "finite I  
-          ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
+          ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
     apply (erule finite_induct)
     apply (simp (no_asm))
     apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
@@ -232,7 +232,7 @@
 
     lemma reachable_PLam_eq: 
      "finite I ==>  
-          reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
+          reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
     apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
     done
 
@@ -240,8 +240,8 @@
     (** Co **)
 
     lemma Constrains_imp_PLam_Constrains: 
-     "[| F i : A Co B;  i: I;  finite I |]   
-          ==> PLam I F : (lift_set i A) Co (lift_set i B)"
+     "[| F i \<in> A Co B;  i \<in> I;  finite I |]   
+          ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
     apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
     apply (auto simp add: constrains_def PLam_def)
     apply (REPEAT (blast intro: reachable.intrs))
@@ -250,15 +250,15 @@
 
 
     lemma PLam_Constrains: 
-     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
-          ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =   
-              (F i : A Co B)"
+     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
+          ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =   
+              (F i \<in> A Co B)"
     apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
     done
 
     lemma PLam_Stable: 
-     "[| i: I;  finite I;  f0: Init (PLam I F) |]   
-          ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
+     "[| i \<in> I;  finite I;  f0: Init (PLam I F) |]   
+          ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
     apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
     done
 
@@ -266,23 +266,23 @@
     (** const_PLam (no dependence on i) doesn't require the f0 premise **)
 
     lemma const_PLam_Constrains: 
-     "[| i: I;  finite I |]   
-          ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =   
-              (F : A Co B)"
+     "[| i \<in> I;  finite I |]   
+          ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =   
+              (F \<in> A Co B)"
     apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
     done
 
     lemma const_PLam_Stable: 
-     "[| i: I;  finite I |]   
-          ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
+     "[| i \<in> I;  finite I |]   
+          ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
     apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
     done
 
     lemma const_PLam_Increasing: 
-	 "[| i: I;  finite I |]   
-          ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"
+	 "[| i \<in> I;  finite I |]   
+          ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
     apply (unfold Increasing_def)
-    apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}")
+    apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
     apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
     apply (simp add: finite_lessThan const_PLam_Stable)
     done
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Rename.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -31,7 +31,7 @@
 apply (erule surj_f_inv_f)
 done
 
-lemma mem_rename_set_iff: "bij h ==> z : h`A = (inv h z : A)"
+lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)"
 by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])
 
 
@@ -176,31 +176,31 @@
 by (simp add: rename_def Extend.extend_Join)
 
 lemma rename_JN [simp]:
-     "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"
+     "bij h ==> rename h (JOIN I F) = (\<Squnion>i \<in> I. rename h (F i))"
 by (simp add: rename_def Extend.extend_JN)
 
 
 subsection{*Strong Safety: co, stable*}
 
 lemma rename_constrains: 
-     "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
+     "bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)"
 apply (unfold rename_def)
 apply (subst extend_set_eq_image [symmetric])+
 apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains])
 done
 
 lemma rename_stable: 
-     "bij h ==> (rename h F : stable (h`A)) = (F : stable A)"
+     "bij h ==> (rename h F \<in> stable (h`A)) = (F \<in> stable A)"
 apply (simp add: stable_def rename_constrains)
 done
 
 lemma rename_invariant:
-     "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)"
+     "bij h ==> (rename h F \<in> invariant (h`A)) = (F \<in> invariant A)"
 apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff])
 done
 
 lemma rename_increasing:
-     "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))"
+     "bij h ==> (rename h F \<in> increasing func) = (F \<in> increasing (func o h))"
 apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f])
 done
 
@@ -213,19 +213,19 @@
 done
 
 lemma rename_Constrains:
-     "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)"
+     "bij h ==> (rename h F \<in> (h`A) Co (h`B)) = (F \<in> A Co B)"
 by (simp add: Constrains_def reachable_rename_eq rename_constrains
                bij_is_inj image_Int [symmetric])
 
 lemma rename_Stable: 
-     "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)"
+     "bij h ==> (rename h F \<in> Stable (h`A)) = (F \<in> Stable A)"
 by (simp add: Stable_def rename_Constrains)
 
-lemma rename_Always: "bij h ==> (rename h F : Always (h`A)) = (F : Always A)"
+lemma rename_Always: "bij h ==> (rename h F \<in> Always (h`A)) = (F \<in> Always A)"
 by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff])
 
 lemma rename_Increasing:
-     "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))"
+     "bij h ==> (rename h F \<in> Increasing func) = (F \<in> Increasing (func o h))"
 by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq 
               bij_is_surj [THEN surj_f_inv_f])
 
@@ -233,52 +233,52 @@
 subsection{*Progress: transient, ensures*}
 
 lemma rename_transient: 
-     "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
+     "bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)"
 apply (unfold rename_def)
 apply (subst extend_set_eq_image [symmetric])
 apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient])
 done
 
 lemma rename_ensures: 
-     "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)"
+     "bij h ==> (rename h F \<in> (h`A) ensures (h`B)) = (F \<in> A ensures B)"
 apply (unfold rename_def)
 apply (subst extend_set_eq_image [symmetric])+
 apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures])
 done
 
 lemma rename_leadsTo: 
-     "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)"
+     "bij h ==> (rename h F \<in> (h`A) leadsTo (h`B)) = (F \<in> A leadsTo B)"
 apply (unfold rename_def)
 apply (subst extend_set_eq_image [symmetric])+
 apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo])
 done
 
 lemma rename_LeadsTo: 
-     "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)"
+     "bij h ==> (rename h F \<in> (h`A) LeadsTo (h`B)) = (F \<in> A LeadsTo B)"
 apply (unfold rename_def)
 apply (subst extend_set_eq_image [symmetric])+
 apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo])
 done
 
 lemma rename_rename_guarantees_eq: 
-     "bij h ==> (rename h F : (rename h ` X) guarantees  
+     "bij h ==> (rename h F \<in> (rename h ` X) guarantees  
                               (rename h ` Y)) =  
-                (F : X guarantees Y)"
+                (F \<in> X guarantees Y)"
 apply (unfold rename_def)
 apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption)
 apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def)
 done
 
 lemma rename_guarantees_eq_rename_inv:
-     "bij h ==> (rename h F : X guarantees Y) =  
-                (F : (rename (inv h) ` X) guarantees  
+     "bij h ==> (rename h F \<in> X guarantees Y) =  
+                (F \<in> (rename (inv h) ` X) guarantees  
                      (rename (inv h) ` Y))"
 apply (subst rename_rename_guarantees_eq [symmetric], assumption)
 apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
 done
 
 lemma rename_preserves:
-     "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"
+     "bij h ==> (rename h G \<in> preserves v) = (G \<in> preserves (v o h))"
 apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption)
 apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f])
 done
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -12,10 +12,10 @@
 
 constdefs
    Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
-    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
+    "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
 
    LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
-    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
+    "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
 
 syntax (xsymbols)
   "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
@@ -23,7 +23,7 @@
 
 (*Resembles the previous definition of LeadsTo*)
 lemma LeadsTo_eq_leadsTo: 
-     "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
+     "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
 apply (unfold LeadsTo_def)
 apply (blast dest: psp_stable2 intro: leadsTo_weaken)
 done
@@ -34,35 +34,37 @@
 (** Conjoining an Always property **)
 
 lemma Always_LeadsTo_pre:
-     "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
-by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+     "F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')"
+by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 
+              Int_assoc [symmetric])
 
 lemma Always_LeadsTo_post:
-     "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
-by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+     "F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')"
+by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 
+              Int_assoc [symmetric])
 
-(* [| F : Always C;  F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
+(* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
 lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
 
-(* [| F : Always INV;  F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
+(* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
 lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
 
 
 subsection{*Introduction rules: Basis, Trans, Union*}
 
-lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
+lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
 apply (simp add: LeadsTo_def)
 apply (blast intro: leadsTo_weaken_L)
 done
 
 lemma LeadsTo_Trans:
-     "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C"
+     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
 apply (simp add: LeadsTo_eq_leadsTo)
 apply (blast intro: leadsTo_Trans)
 done
 
 lemma LeadsTo_Union: 
-     "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
+     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
 apply (simp add: LeadsTo_def)
 apply (subst Int_Union)
 apply (blast intro: leadsTo_UN)
@@ -71,37 +73,37 @@
 
 subsection{*Derived rules*}
 
-lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
+lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
 by (simp add: LeadsTo_def)
 
 (*Useful with cancellation, disjunction*)
 lemma LeadsTo_Un_duplicate:
-     "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"
+     "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
 by (simp add: Un_ac)
 
 lemma LeadsTo_Un_duplicate2:
-     "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"
+     "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
 by (simp add: Un_ac)
 
 lemma LeadsTo_UN: 
-     "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
+     "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
 apply (simp only: Union_image_eq [symmetric])
 apply (blast intro: LeadsTo_Union)
 done
 
 (*Binary union introduction rule*)
 lemma LeadsTo_Un:
-     "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"
+     "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
 apply (subst Un_eq_Union)
 apply (blast intro: LeadsTo_Union)
 done
 
 (*Lets us look at the starting state*)
 lemma single_LeadsTo_I:
-     "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
+     "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
 by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
 
-lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
+lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B"
 apply (simp add: LeadsTo_def)
 apply (blast intro: subset_imp_leadsTo)
 done
@@ -109,73 +111,73 @@
 lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
 
 lemma LeadsTo_weaken_R [rule_format]:
-     "[| F : A LeadsTo A';  A' <= B' |] ==> F : A LeadsTo B'"
-apply (simp (no_asm_use) add: LeadsTo_def)
+     "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
+apply (simp add: LeadsTo_def)
 apply (blast intro: leadsTo_weaken_R)
 done
 
 lemma LeadsTo_weaken_L [rule_format]:
-     "[| F : A LeadsTo A';  B <= A |]   
-      ==> F : B LeadsTo A'"
-apply (simp (no_asm_use) add: LeadsTo_def)
+     "[| F \<in> A LeadsTo A';  B \<subseteq> A |]   
+      ==> F \<in> B LeadsTo A'"
+apply (simp add: LeadsTo_def)
 apply (blast intro: leadsTo_weaken_L)
 done
 
 lemma LeadsTo_weaken:
-     "[| F : A LeadsTo A';    
-         B  <= A;   A' <= B' |]  
-      ==> F : B LeadsTo B'"
+     "[| F \<in> A LeadsTo A';    
+         B  \<subseteq> A;   A' \<subseteq> B' |]  
+      ==> F \<in> B LeadsTo B'"
 by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
 
 lemma Always_LeadsTo_weaken:
-     "[| F : Always C;  F : A LeadsTo A';    
-         C Int B <= A;   C Int A' <= B' |]  
-      ==> F : B LeadsTo B'"
+     "[| F \<in> Always C;  F \<in> A LeadsTo A';    
+         C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
+      ==> F \<in> B LeadsTo B'"
 by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
 
 (** Two theorems for "proof lattices" **)
 
-lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"
+lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B"
 by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
 
 lemma LeadsTo_Trans_Un:
-     "[| F : A LeadsTo B;  F : B LeadsTo C |]  
-      ==> F : (A Un B) LeadsTo C"
+     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]  
+      ==> F \<in> (A \<union> B) LeadsTo C"
 by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
 
 
 (** Distributive laws **)
 
 lemma LeadsTo_Un_distrib:
-     "(F : (A Un B) LeadsTo C)  = (F : A LeadsTo C & F : B LeadsTo C)"
+     "(F \<in> (A \<union> B) LeadsTo C)  = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
 by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
 
 lemma LeadsTo_UN_distrib:
-     "(F : (UN i:I. A i) LeadsTo B)  =  (ALL i : I. F : (A i) LeadsTo B)"
+     "(F \<in> (\<Union>i \<in> I. A i) LeadsTo B)  =  (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)"
 by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
 
 lemma LeadsTo_Union_distrib:
-     "(F : (Union S) LeadsTo B)  =  (ALL A : S. F : A LeadsTo B)"
+     "(F \<in> (Union S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
 by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
 
 
 (** More rules using the premise "Always INV" **)
 
-lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
+lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
 by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
 
 lemma EnsuresI:
-     "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]    
-      ==> F : A Ensures B"
+     "[| F \<in> (A-B) Co (A \<union> B);  F \<in> transient (A-B) |]    
+      ==> F \<in> A Ensures B"
 apply (simp add: Ensures_def Constrains_eq_constrains)
 apply (blast intro: ensuresI constrains_weaken transient_strengthen)
 done
 
 lemma Always_LeadsTo_Basis:
-     "[| F : Always INV;       
-         F : (INV Int (A-A')) Co (A Un A');  
-         F : transient (INV Int (A-A')) |]    
-  ==> F : A LeadsTo A'"
+     "[| F \<in> Always INV;       
+         F \<in> (INV \<inter> (A-A')) Co (A \<union> A');  
+         F \<in> transient (INV \<inter> (A-A')) |]    
+  ==> F \<in> A LeadsTo A'"
 apply (rule Always_LeadsToI, assumption)
 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
 done
@@ -183,14 +185,14 @@
 (*Set difference: maybe combine with leadsTo_weaken_L??
   This is the most useful form of the "disjunction" rule*)
 lemma LeadsTo_Diff:
-     "[| F : (A-B) LeadsTo C;  F : (A Int B) LeadsTo C |]  
-      ==> F : A LeadsTo C"
+     "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
+      ==> F \<in> A LeadsTo C"
 by (blast intro: LeadsTo_Un LeadsTo_weaken)
 
 
 lemma LeadsTo_UN_UN: 
-     "(!! i. i:I ==> F : (A i) LeadsTo (A' i))  
-      ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"
+     "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))  
+      ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
 apply (simp only: Union_image_eq [symmetric])
 apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
 done
@@ -198,48 +200,47 @@
 
 (*Version with no index set*)
 lemma LeadsTo_UN_UN_noindex: 
-     "(!! i. F : (A i) LeadsTo (A' i))  
-      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+     "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
 by (blast intro: LeadsTo_UN_UN)
 
 (*Version with no index set*)
 lemma all_LeadsTo_UN_UN:
-     "ALL i. F : (A i) LeadsTo (A' i)  
-      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+     "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
+      ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
 by (blast intro: LeadsTo_UN_UN)
 
 (*Binary union version*)
 lemma LeadsTo_Un_Un:
-     "[| F : A LeadsTo A'; F : B LeadsTo B' |]  
-            ==> F : (A Un B) LeadsTo (A' Un B')"
+     "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
+            ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
 by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
 
 
 (** The cancellation law **)
 
 lemma LeadsTo_cancel2:
-     "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]     
-      ==> F : A LeadsTo (A' Un B')"
+     "[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |]     
+      ==> F \<in> A LeadsTo (A' \<union> B')"
 by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans)
 
 lemma LeadsTo_cancel_Diff2:
-     "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |]  
-      ==> F : A LeadsTo (A' Un B')"
+     "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |]  
+      ==> F \<in> A LeadsTo (A' \<union> B')"
 apply (rule LeadsTo_cancel2)
 prefer 2 apply assumption
 apply (simp_all (no_asm_simp))
 done
 
 lemma LeadsTo_cancel1:
-     "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |]  
-      ==> F : A LeadsTo (B' Un A')"
+     "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |]  
+      ==> F \<in> A LeadsTo (B' \<union> A')"
 apply (simp add: Un_commute)
 apply (blast intro!: LeadsTo_cancel2)
 done
 
 lemma LeadsTo_cancel_Diff1:
-     "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |]  
-      ==> F : A LeadsTo (B' Un A')"
+     "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |]  
+      ==> F \<in> A LeadsTo (B' \<union> A')"
 apply (rule LeadsTo_cancel1)
 prefer 2 apply assumption
 apply (simp_all (no_asm_simp))
@@ -249,8 +250,8 @@
 (** The impossibility law **)
 
 (*The set "A" may be non-empty, but it contains no reachable states*)
-lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
-apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
+lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
+apply (simp add: LeadsTo_def Always_eq_includes_reachable)
 apply (drule leadsTo_empty, auto)
 done
 
@@ -259,33 +260,33 @@
 
 (*Special case of PSP: Misra's "stable conjunction"*)
 lemma PSP_Stable:
-     "[| F : A LeadsTo A';  F : Stable B |]  
-      ==> F : (A Int B) LeadsTo (A' Int B)"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable)
+     "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
+      ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
+apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable)
 apply (drule psp_stable, assumption)
 apply (simp add: Int_ac)
 done
 
 lemma PSP_Stable2:
-     "[| F : A LeadsTo A'; F : Stable B |]  
-      ==> F : (B Int A) LeadsTo (B Int A')"
+     "[| F \<in> A LeadsTo A'; F \<in> Stable B |]  
+      ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
 by (simp add: PSP_Stable Int_ac)
 
 lemma PSP:
-     "[| F : A LeadsTo A'; F : B Co B' |]  
-      ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
-apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
+     "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
+      ==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
+apply (simp add: LeadsTo_def Constrains_eq_constrains)
 apply (blast dest: psp intro: leadsTo_weaken)
 done
 
 lemma PSP2:
-     "[| F : A LeadsTo A'; F : B Co B' |]  
-      ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
+     "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
+      ==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
 by (simp add: PSP Int_ac)
 
 lemma PSP_Unless: 
-     "[| F : A LeadsTo A'; F : B Unless B' |]  
-      ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"
+     "[| F \<in> A LeadsTo A'; F \<in> B Unless B' |]  
+      ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
 apply (unfold Unless_def)
 apply (drule PSP, assumption)
 apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
@@ -293,8 +294,8 @@
 
 
 lemma Stable_transient_Always_LeadsTo:
-     "[| F : Stable A;  F : transient C;   
-         F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
+     "[| F \<in> Stable A;  F \<in> transient C;   
+         F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B"
 apply (erule Always_LeadsTo_weaken)
 apply (rule LeadsTo_Diff)
    prefer 2
@@ -309,10 +310,10 @@
 (** Meta or object quantifier ????? **)
 lemma LeadsTo_wf_induct:
      "[| wf r;      
-         ALL m. F : (A Int f-`{m}) LeadsTo                      
-                            ((A Int f-`(r^-1 `` {m})) Un B) |]  
-      ==> F : A LeadsTo B"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo)
+         \<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo                      
+                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+      ==> F \<in> A LeadsTo B"
+apply (simp add: LeadsTo_eq_leadsTo)
 apply (erule leadsTo_wf_induct)
 apply (blast intro: leadsTo_weaken)
 done
@@ -320,28 +321,27 @@
 
 lemma Bounded_induct:
      "[| wf r;      
-         ALL m:I. F : (A Int f-`{m}) LeadsTo                    
-                              ((A Int f-`(r^-1 `` {m})) Un B) |]  
-      ==> F : A LeadsTo ((A - (f-`I)) Un B)"
+         \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo                    
+                      ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+      ==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)"
 apply (erule LeadsTo_wf_induct, safe)
-apply (case_tac "m:I")
+apply (case_tac "m \<in> I")
 apply (blast intro: LeadsTo_weaken)
 apply (blast intro: subset_imp_LeadsTo)
 done
 
 
 lemma LessThan_induct:
-     "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))  
-      ==> F : A LeadsTo B"
-apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
-done
+     "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B))
+      ==> F \<in> A LeadsTo B"
+by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
 
 (*Integer version.  Could generalize from 0 to any lower bound*)
 lemma integ_0_le_induct:
-     "[| F : Always {s. (0::int) <= f s};   
-         !! z. F : (A Int {s. f s = z}) LeadsTo                      
-                            ((A Int {s. f s < z}) Un B) |]  
-      ==> F : A LeadsTo B"
+     "[| F \<in> Always {s. (0::int) \<le> f s};   
+         !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo                      
+                   ((A \<inter> {s. f s < z}) \<union> B) |]  
+      ==> F \<in> A LeadsTo B"
 apply (rule_tac f = "nat o f" in LessThan_induct)
 apply (simp add: vimage_def)
 apply (rule Always_LeadsTo_weaken, assumption+)
@@ -349,42 +349,42 @@
 done
 
 lemma LessThan_bounded_induct:
-     "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo    
-                                         ((A Int f-`(lessThan m)) Un B) |]  
-            ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)"
-apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
-apply (rule wf_less_than [THEN Bounded_induct])
-apply (simp (no_asm_simp))
+     "!!l::nat. \<forall>m \<in> greaterThan l. 
+                   F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)
+            ==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
+apply (simp only: Diff_eq [symmetric] vimage_Compl 
+                  Compl_greaterThan [symmetric])
+apply (rule wf_less_than [THEN Bounded_induct], simp)
 done
 
 lemma GreaterThan_bounded_induct:
-     "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo    
-                               ((A Int f-`(greaterThan m)) Un B) |]  
-      ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)"
+     "!!l::nat. \<forall>m \<in> lessThan l. 
+                 F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)
+      ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
 apply (rule_tac f = f and f1 = "%k. l - k" 
        in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
 apply (simp add: inv_image_def Image_singleton, clarify)
 apply (case_tac "m<l")
- prefer 2 apply (blast intro: not_leE subset_imp_LeadsTo)
-apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
+ apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
+apply (blast intro: not_leE subset_imp_LeadsTo)
 done
 
 
 subsection{*Completion: Binary and General Finite versions*}
 
 lemma Completion:
-     "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);  
-         F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |]  
-      ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
+     "[| F \<in> A LeadsTo (A' \<union> C);  F \<in> A' Co (A' \<union> C);  
+         F \<in> B LeadsTo (B' \<union> C);  F \<in> B' Co (B' \<union> C) |]  
+      ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
+apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
 apply (blast intro: completion leadsTo_weaken)
 done
 
 lemma Finite_completion_lemma:
      "finite I  
-      ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->   
-          (ALL i:I. F : (A' i) Co (A' i Un C)) -->  
-          F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
+      ==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) -->   
+          (\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) -->  
+          F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
 apply (erule finite_induct, auto)
 apply (rule Completion)
    prefer 4
@@ -394,15 +394,15 @@
 
 lemma Finite_completion: 
      "[| finite I;   
-         !!i. i:I ==> F : (A i) LeadsTo (A' i Un C);  
-         !!i. i:I ==> F : (A' i) Co (A' i Un C) |]    
-      ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
+         !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C);  
+         !!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |]    
+      ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
 by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
 
 lemma Stable_completion: 
-     "[| F : A LeadsTo A';  F : Stable A';    
-         F : B LeadsTo B';  F : Stable B' |]  
-      ==> F : (A Int B) LeadsTo (A' Int B')"
+     "[| F \<in> A LeadsTo A';  F \<in> Stable A';    
+         F \<in> B LeadsTo B';  F \<in> Stable B' |]  
+      ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
 apply (unfold Stable_def)
 apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
 apply (force+)
@@ -410,14 +410,12 @@
 
 lemma Finite_stable_completion: 
      "[| finite I;   
-         !!i. i:I ==> F : (A i) LeadsTo (A' i);  
-         !!i. i:I ==> F : Stable (A' i) |]    
-      ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)"
+         !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i);  
+         !!i. i \<in> I ==> F \<in> Stable (A' i) |]    
+      ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)"
 apply (unfold Stable_def)
 apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
-apply (simp_all (no_asm_simp))
-apply blast+
+apply (simp_all, blast+)
 done
 
-
 end
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -14,15 +14,15 @@
 
 typedef (Program)
   'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
-		   allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" 
+		   allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}" 
   by blast
 
 constdefs
   constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
-    "A co B == {F. ALL act: Acts F. act``A <= B}"
+    "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
 
   unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
-    "A unless B == (A-B) co (A Un B)"
+    "A unless B == (A-B) co (A \<union> B)"
 
   mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
 		   => 'a program"
@@ -39,20 +39,20 @@
     "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
 
   Allowed :: "'a program => 'a program set"
-    "Allowed F == {G. Acts G <= AllowedActs F}"
+    "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
 
   stable     :: "'a set => 'a program set"
     "stable A == A co A"
 
   strongest_rhs :: "['a program, 'a set] => 'a set"
-    "strongest_rhs F A == Inter {B. F : A co B}"
+    "strongest_rhs F A == Inter {B. F \<in> A co B}"
 
   invariant :: "'a set => 'a program set"
-    "invariant A == {F. Init F <= A} Int stable A"
+    "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
 
-  (*Polymorphic in both states and the meaning of <= *)
+  (*Polymorphic in both states and the meaning of \<le> *)
   increasing :: "['a => 'b::{order}] => 'a program set"
-    "increasing f == INT z. stable {s. z <= f s}"
+    "increasing f == \<Inter>z. stable {s. z \<le> f s}"
 
 
 (*Perhaps equalities.ML shouldn't add this in the first place!*)
@@ -64,7 +64,7 @@
      Rep_Program Rep_Program_inverse Abs_Program_inverse 
      Program_def Init_def Acts_def AllowedActs_def mk_program_def
 
-lemma Id_in_Acts [iff]: "Id : Acts F"
+lemma Id_in_Acts [iff]: "Id \<in> Acts F"
 apply (cut_tac x = F in Rep_Program)
 apply (auto simp add: program_typedef) 
 done
@@ -72,7 +72,7 @@
 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
 by (simp add: insert_absorb Id_in_Acts)
 
-lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F"
+lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
 apply (cut_tac x = F in Rep_Program)
 apply (auto simp add: program_typedef) 
 done
@@ -145,114 +145,114 @@
 
 (*An action is expanded only if a pair of states is being tested against it*)
 lemma def_act_simp:
-     "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"
+     "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
 by auto
 
 (*A set is expanded only if an element is being tested against it*)
-lemma def_set_simp: "A == B ==> (x : A) = (x : B)"
+lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
 by auto
 
 
 (*** co ***)
 
 lemma constrainsI: 
-    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
-     ==> F : A co A'"
+    "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
+     ==> F \<in> A co A'"
 by (simp add: constrains_def, blast)
 
 lemma constrainsD: 
-    "[| F : A co A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'"
+    "[| F \<in> A co A'; act: Acts F;  (s,s'): act;  s \<in> A |] ==> s': A'"
 by (unfold constrains_def, blast)
 
-lemma constrains_empty [iff]: "F : {} co B"
+lemma constrains_empty [iff]: "F \<in> {} co B"
 by (unfold constrains_def, blast)
 
-lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})"
+lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
 by (unfold constrains_def, blast)
 
-lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)"
+lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
 by (unfold constrains_def, blast)
 
-lemma constrains_UNIV2 [iff]: "F : A co UNIV"
+lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
 by (unfold constrains_def, blast)
 
 (*monotonic in 2nd argument*)
 lemma constrains_weaken_R: 
-    "[| F : A co A'; A'<=B' |] ==> F : A co B'"
+    "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
 by (unfold constrains_def, blast)
 
 (*anti-monotonic in 1st argument*)
 lemma constrains_weaken_L: 
-    "[| F : A co A'; B<=A |] ==> F : B co A'"
+    "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
 by (unfold constrains_def, blast)
 
 lemma constrains_weaken: 
-   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"
+   "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
 by (unfold constrains_def, blast)
 
 (** Union **)
 
 lemma constrains_Un: 
-    "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"
+    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
 by (unfold constrains_def, blast)
 
 lemma constrains_UN: 
-    "(!!i. i:I ==> F : (A i) co (A' i)) 
-     ==> F : (UN i:I. A i) co (UN i:I. A' i)"
+    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
+     ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
 by (unfold constrains_def, blast)
 
-lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)"
+lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
 by (unfold constrains_def, blast)
 
-lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)"
+lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
 by (unfold constrains_def, blast)
 
-lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)"
+lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
 by (unfold constrains_def, blast)
 
-lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)"
+lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
 by (unfold constrains_def, blast)
 
 (** Intersection **)
 
 lemma constrains_Int: 
-    "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"
+    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
 by (unfold constrains_def, blast)
 
 lemma constrains_INT: 
-    "(!!i. i:I ==> F : (A i) co (A' i)) 
-     ==> F : (INT i:I. A i) co (INT i:I. A' i)"
+    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
+     ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
 by (unfold constrains_def, blast)
 
-lemma constrains_imp_subset: "F : A co A' ==> A <= A'"
+lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
 by (unfold constrains_def, auto)
 
 (*The reasoning is by subsets since "co" refers to single actions
   only.  So this rule isn't that useful.*)
 lemma constrains_trans: 
-    "[| F : A co B; F : B co C |] ==> F : A co C"
+    "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
 by (unfold constrains_def, blast)
 
 lemma constrains_cancel: 
-   "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"
+   "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
 by (unfold constrains_def, clarify, blast)
 
 
 (*** unless ***)
 
-lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B"
+lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
 by (unfold unless_def, assumption)
 
-lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)"
+lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
 by (unfold unless_def, assumption)
 
 
 (*** stable ***)
 
-lemma stableI: "F : A co A ==> F : stable A"
+lemma stableI: "F \<in> A co A ==> F \<in> stable A"
 by (unfold stable_def, assumption)
 
-lemma stableD: "F : stable A ==> F : A co A"
+lemma stableD: "F \<in> stable A ==> F \<in> A co A"
 by (unfold stable_def, assumption)
 
 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
@@ -261,14 +261,14 @@
 (** Union **)
 
 lemma stable_Un: 
-    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"
+    "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
 
 apply (unfold stable_def)
 apply (blast intro: constrains_Un)
 done
 
 lemma stable_UN: 
-    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
 apply (unfold stable_def)
 apply (blast intro: constrains_UN)
 done
@@ -276,75 +276,75 @@
 (** Intersection **)
 
 lemma stable_Int: 
-    "[| F : stable A;  F : stable A' |] ==> F : stable (A Int A')"
+    "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
 apply (unfold stable_def)
 apply (blast intro: constrains_Int)
 done
 
 lemma stable_INT: 
-    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)"
+    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
 apply (unfold stable_def)
 apply (blast intro: constrains_INT)
 done
 
 lemma stable_constrains_Un: 
-    "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"
+    "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
 by (unfold stable_def constrains_def, blast)
 
 lemma stable_constrains_Int: 
-  "[| F : stable C; F :  (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"
+  "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
 by (unfold stable_def constrains_def, blast)
 
-(*[| F : stable C; F :  (C Int A) co A |] ==> F : stable (C Int A) *)
+(*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
 lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
 
 
 (*** invariant ***)
 
-lemma invariantI: "[| Init F<=A;  F: stable A |] ==> F : invariant A"
+lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
 by (simp add: invariant_def)
 
-(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+(*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
 lemma invariant_Int:
-     "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)"
+     "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
 by (auto simp add: invariant_def stable_Int)
 
 
 (*** increasing ***)
 
 lemma increasingD: 
-     "F : increasing f ==> F : stable {s. z <= f s}"
+     "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
 
 by (unfold increasing_def, blast)
 
-lemma increasing_constant [iff]: "F : increasing (%s. c)"
+lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
 by (unfold increasing_def stable_def, auto)
 
 lemma mono_increasing_o: 
-     "mono g ==> increasing f <= increasing (g o f)"
+     "mono g ==> increasing f \<subseteq> increasing (g o f)"
 apply (unfold increasing_def stable_def constrains_def, auto)
 apply (blast intro: monoD order_trans)
 done
 
-(*Holds by the theorem (Suc m <= n) = (m < n) *)
+(*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
 lemma strict_increasingD: 
-     "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"
+     "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
 by (simp add: increasing_def Suc_le_eq [symmetric])
 
 
 (** The Elimination Theorem.  The "free" m has become universally quantified!
-    Should the premise be !!m instead of ALL m ?  Would make it harder to use
+    Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
     in forward proof. **)
 
 lemma elimination: 
-    "[| ALL m:M. F : {s. s x = m} co (B m) |]  
-     ==> F : {s. s x : M} co (UN m:M. B m)"
+    "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]  
+     ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
 (*As above, but for the trivial case of a one-variable state, in which the
   state is identified with its one variable.*)
 lemma elimination_sing: 
-    "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"
+    "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
 
@@ -352,20 +352,20 @@
 (*** Theoretical Results from Section 6 ***)
 
 lemma constrains_strongest_rhs: 
-    "F : A co (strongest_rhs F A )"
+    "F \<in> A co (strongest_rhs F A )"
 by (unfold constrains_def strongest_rhs_def, blast)
 
 lemma strongest_rhs_is_strongest: 
-    "F : A co B ==> strongest_rhs F A <= B"
+    "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
 by (unfold constrains_def strongest_rhs_def, blast)
 
 
 (** Ad-hoc set-theory rules **)
 
-lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B"
+lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
 by blast
 
-lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)"
+lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
 by blast
 
 (** Needed for WF reasoning in WFair.ML **)
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Union.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -12,36 +12,36 @@
 
 constdefs
 
-  (*FIXME: conjoin Init F Int Init G ~= {} *) 
+  (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
   ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
-    "F ok G == Acts F <= AllowedActs G &
-               Acts G <= AllowedActs F"
+    "F ok G == Acts F \<subseteq> AllowedActs G &
+               Acts G \<subseteq> AllowedActs F"
 
-  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
+  (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
   OK  :: "['a set, 'a => 'b program] => bool"
-    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
+    "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
 
   JOIN  :: "['a set, 'a => 'b program] => 'b program"
-    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
-			     INT i:I. AllowedActs (F i))"
+    "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
+			     \<Inter>i \<in> I. AllowedActs (F i))"
 
   Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
-    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
-			     AllowedActs F Int AllowedActs G)"
+    "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+			     AllowedActs F \<inter> AllowedActs G)"
 
   SKIP :: "'a program"
     "SKIP == mk_program (UNIV, {}, UNIV)"
 
   (*Characterizes safety properties.  Used with specifying AllowedActs*)
   safety_prop :: "'a program set => bool"
-    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
+    "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
 syntax
   "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
 
 translations
-  "JN x:A. B"   == "JOIN A (%x. B)"
+  "JN x : A. B"   == "JOIN A (%x. B)"
   "JN x y. B"   == "JN x. JN y. B"
   "JN x. B"     == "JOIN UNIV (%x. B)"
 
@@ -49,7 +49,7 @@
   SKIP      :: "'a program"                              ("\<bottom>")
   "op Join" :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
   "@JOIN1"  :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
-  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _:_./ _)" 10)
+  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
 
 
 subsection{*SKIP*}
@@ -68,13 +68,13 @@
 
 subsection{*SKIP and safety properties*}
 
-lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
+lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
 by (unfold constrains_def, auto)
 
-lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
+lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)"
 by (unfold Constrains_def, auto)
 
-lemma SKIP_in_stable [iff]: "SKIP : stable A"
+lemma SKIP_in_stable [iff]: "SKIP \<in> stable A"
 by (unfold stable_def, auto)
 
 declare SKIP_in_stable [THEN stable_imp_Stable, iff]
@@ -82,40 +82,40 @@
 
 subsection{*Join*}
 
-lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
+lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G"
 by (simp add: Join_def)
 
-lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
+lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G"
 by (auto simp add: Join_def)
 
 lemma AllowedActs_Join [simp]:
-     "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
+     "AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G"
 by (auto simp add: Join_def)
 
 
 subsection{*JN*}
 
-lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
+lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
 by (unfold JOIN_def SKIP_def, auto)
 
-lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
+lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)"
 apply (rule program_equalityI)
 apply (auto simp add: JOIN_def Join_def)
 done
 
-lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
+lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))"
 by (simp add: JOIN_def)
 
-lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
+lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))"
 by (auto simp add: JOIN_def)
 
 lemma AllowedActs_JN [simp]:
-     "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
+     "AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))"
 by (auto simp add: JOIN_def)
 
 
 lemma JN_cong [cong]: 
-    "[| I=J;  !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
+    "[| I=J;  !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)"
 by (simp add: JOIN_def)
 
 
@@ -156,28 +156,28 @@
 lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
 
 
-subsection{*JN laws*}
+subsection{*\<Squnion>laws*}
 
 (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
-lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
+lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
 by (auto intro!: program_equalityI)
 
-lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
+lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))"
 by (auto intro!: program_equalityI)
 
-lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
+lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
 by (rule program_equalityI, auto)
 
 lemma JN_Join_distrib:
-     "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)"
+     "(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i)  Join  (\<Squnion>i \<in> I. G i)"
 by (auto intro!: program_equalityI)
 
 lemma JN_Join_miniscope:
-     "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
+     "i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)"
 by (auto simp add: JN_Join_distrib JN_constant)
 
 (*Used to prove guarantees_JN_I*)
-lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
+lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F"
 apply (unfold JOIN_def Join_def)
 apply (rule program_equalityI, auto)
 done
@@ -185,19 +185,19 @@
 
 subsection{*Safety: co, stable, FP*}
 
-(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
-  alternative precondition is A<=B, but most proofs using this rule require
+(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B.  So an
+  alternative precondition is A \<subseteq> B, but most proofs using this rule require
   I to be nonempty for other reasons anyway.*)
 lemma JN_constrains: 
-    "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
+    "i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)"
 by (simp add: constrains_def JOIN_def, blast)
 
 lemma Join_constrains [simp]:
-     "(F Join G : A co B) = (F : A co B & G : A co B)"
+     "(F Join G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
 by (auto simp add: constrains_def Join_def)
 
 lemma Join_unless [simp]:
-     "(F Join G : A unless B) = (F : A unless B & G : A unless B)"
+     "(F Join G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
 by (simp add: Join_constrains unless_def)
 
 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
@@ -206,100 +206,100 @@
 
 
 lemma Join_constrains_weaken:
-     "[| F : A co A';  G : B co B' |]  
-      ==> F Join G : (A Int B) co (A' Un B')"
+     "[| F \<in> A co A';  G \<in> B co B' |]  
+      ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
 by (simp, blast intro: constrains_weaken)
 
-(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
+(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
 lemma JN_constrains_weaken:
-     "[| ALL i:I. F i : A i co A' i;  i: I |]  
-      ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"
+     "[| \<forall>i \<in> I. F i \<in> A i co A' i;  i \<in> I |]  
+      ==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
 apply (simp (no_asm_simp) add: JN_constrains)
 apply (blast intro: constrains_weaken)
 done
 
-lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
+lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)"
 by (simp add: stable_def constrains_def JOIN_def)
 
 lemma invariant_JN_I:
-     "[| !!i. i:I ==> F i : invariant A;  i : I |]   
-       ==> (JN i:I. F i) : invariant A"
+     "[| !!i. i \<in> I ==> F i \<in> invariant A;  i \<in> I |]   
+       ==> (\<Squnion>i \<in> I. F i) \<in> invariant A"
 by (simp add: invariant_def JN_stable, blast)
 
 lemma Join_stable [simp]:
-     "(F Join G : stable A) =  
-      (F : stable A & G : stable A)"
+     "(F Join G \<in> stable A) =  
+      (F \<in> stable A & G \<in> stable A)"
 by (simp add: stable_def)
 
 lemma Join_increasing [simp]:
-     "(F Join G : increasing f) =  
-      (F : increasing f & G : increasing f)"
+     "(F Join G \<in> increasing f) =  
+      (F \<in> increasing f & G \<in> increasing f)"
 by (simp add: increasing_def Join_stable, blast)
 
 lemma invariant_JoinI:
-     "[| F : invariant A; G : invariant A |]   
-      ==> F Join G : invariant A"
+     "[| F \<in> invariant A; G \<in> invariant A |]   
+      ==> F Join G \<in> invariant A"
 by (simp add: invariant_def, blast)
 
-lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
+lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
 by (simp add: FP_def JN_stable INTER_def)
 
 
 subsection{*Progress: transient, ensures*}
 
 lemma JN_transient:
-     "i : I ==>  
-    (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
+     "i \<in> I ==>  
+    (\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)"
 by (auto simp add: transient_def JOIN_def)
 
 lemma Join_transient [simp]:
-     "F Join G : transient A =  
-      (F : transient A | G : transient A)"
+     "F Join G \<in> transient A =  
+      (F \<in> transient A | G \<in> transient A)"
 by (auto simp add: bex_Un transient_def Join_def)
 
-lemma Join_transient_I1: "F : transient A ==> F Join G : transient A"
+lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A"
 by (simp add: Join_transient)
 
-lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
+lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A"
 by (simp add: Join_transient)
 
-(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
+(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
 lemma JN_ensures:
-     "i : I ==>  
-      (JN i:I. F i) : A ensures B =  
-      ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
+     "i \<in> I ==>  
+      (\<Squnion>i \<in> I. F i) \<in> A ensures B =  
+      ((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))"
 by (auto simp add: ensures_def JN_constrains JN_transient)
 
 lemma Join_ensures: 
-     "F Join G : A ensures B =      
-      (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &  
-       (F : transient (A-B) | G : transient (A-B)))"
+     "F Join G \<in> A ensures B =      
+      (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
+       (F \<in> transient (A-B) | G \<in> transient (A-B)))"
 by (auto simp add: ensures_def Join_transient)
 
 lemma stable_Join_constrains: 
-    "[| F : stable A;  G : A co A' |]  
-     ==> F Join G : A co A'"
+    "[| F \<in> stable A;  G \<in> A co A' |]  
+     ==> F Join G \<in> A co A'"
 apply (unfold stable_def constrains_def Join_def)
 apply (simp add: ball_Un, blast)
 done
 
-(*Premise for G cannot use Always because  F: Stable A  is weaker than
-  G : stable A *)
+(*Premise for G cannot use Always because  F \<in> Stable A  is weaker than
+  G \<in> stable A *)
 lemma stable_Join_Always1:
-     "[| F : stable A;  G : invariant A |] ==> F Join G : Always A"
+     "[| F \<in> stable A;  G \<in> invariant A |] ==> F Join G \<in> Always A"
 apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
 apply (force intro: stable_Int)
 done
 
 (*As above, but exchanging the roles of F and G*)
 lemma stable_Join_Always2:
-     "[| F : invariant A;  G : stable A |] ==> F Join G : Always A"
+     "[| F \<in> invariant A;  G \<in> stable A |] ==> F Join G \<in> Always A"
 apply (subst Join_commute)
 apply (blast intro: stable_Join_Always1)
 done
 
 lemma stable_Join_ensures1:
-     "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B"
+     "[| F \<in> stable A;  G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
 apply (simp (no_asm_simp) add: Join_ensures)
 apply (simp add: stable_def ensures_def)
 apply (erule constrains_weaken, auto)
@@ -307,7 +307,7 @@
 
 (*As above, but exchanging the roles of F and G*)
 lemma stable_Join_ensures2:
-     "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B"
+     "[| F \<in> A ensures B;  G \<in> stable A |] ==> F Join G \<in> A ensures B"
 apply (subst Join_commute)
 apply (blast intro: stable_Join_ensures1)
 done
@@ -344,16 +344,16 @@
 lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
 by (auto simp add: ok_def)
 
-lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
+lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
 by (auto simp add: ok_def)
 
-lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (ALL i:I. G i ok F)"
+lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (\<forall>i \<in> I. G i ok F)"
 by (auto simp add: ok_def)
 
-lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
+lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))"
 by (auto simp add: ok_def OK_def)
 
-lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
+lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)"
 by (auto simp add: OK_iff_ok)
 
 
@@ -362,27 +362,27 @@
 lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
 by (auto simp add: Allowed_def)
 
-lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
+lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G"
 by (auto simp add: Allowed_def)
 
-lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
+lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
 by (auto simp add: Allowed_def)
 
-lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
+lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)"
 by (simp add: ok_def Allowed_def)
 
-lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
+lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
 by (auto simp add: OK_iff_ok ok_iff_Allowed)
 
 subsection{*@{text safety_prop}, for reasoning about
  given instances of "ok"*}
 
 lemma safety_prop_Acts_iff:
-     "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
+     "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
 by (auto simp add: safety_prop_def)
 
 lemma safety_prop_AllowedActs_iff_Allowed:
-     "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
+     "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
 by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
 
 lemma Allowed_eq:
@@ -395,27 +395,27 @@
 by (simp add: Allowed_eq)
 
 (*For safety_prop to hold, the property must be satisfiable!*)
-lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
+lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
 by (simp add: safety_prop_def constrains_def, blast)
 
 lemma safety_prop_stable [iff]: "safety_prop (stable A)"
 by (simp add: stable_def)
 
 lemma safety_prop_Int [simp]:
-     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
+     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
 by (simp add: safety_prop_def, blast)
 
 lemma safety_prop_INTER1 [simp]:
-     "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
+     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
 by (auto simp add: safety_prop_def, blast)
 							       
 lemma safety_prop_INTER [simp]:
-     "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
+     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
 by (auto simp add: safety_prop_def, blast)
 
 lemma def_UNION_ok_iff:
      "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
-      ==> F ok G = (G : X & acts <= AllowedActs G)"
+      ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
 by (auto simp add: ok_def safety_prop_Acts_iff)
 
 end
diff -r d643300e4fc0 -r 3786b2fd6808 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/WFair.thy	Tue Feb 04 18:12:40 2003 +0100
@@ -17,10 +17,10 @@
   (*This definition specifies weak fairness.  The rest of the theory
     is generic to all forms of fairness.*)
   transient :: "'a set => 'a program set"
-    "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
+    "transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}"
 
   ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
-    "A ensures B == (A-B co A Un B) Int transient (A-B)"
+    "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
 
 
 consts
@@ -32,22 +32,22 @@
 inductive "leads F"
   intros 
 
-    Basis:  "F : A ensures B ==> (A,B) : leads F"
+    Basis:  "F \<in> A ensures B ==> (A,B) \<in> leads F"
 
-    Trans:  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
+    Trans:  "[| (A,B) \<in> leads F;  (B,C) \<in> leads F |] ==> (A,C) \<in> leads F"
 
-    Union:  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
+    Union:  "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
 
 
 constdefs
 
   (*visible version of the LEADS-TO relation*)
   leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
-    "A leadsTo B == {F. (A,B) : leads F}"
+    "A leadsTo B == {F. (A,B) \<in> leads F}"
   
   (*wlt F B is the largest set that leads to B*)
   wlt :: "['a program, 'a set] => 'a set"
-    "wlt F B == Union {A. F: A leadsTo B}"
+    "wlt F B == Union {A. F \<in> A leadsTo B}"
 
 syntax (xsymbols)
   "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
@@ -56,22 +56,22 @@
 subsection{*transient*}
 
 lemma stable_transient_empty: 
-    "[| F : stable A; F : transient A |] ==> A = {}"
+    "[| F \<in> stable A; F \<in> transient A |] ==> A = {}"
 by (unfold stable_def constrains_def transient_def, blast)
 
 lemma transient_strengthen: 
-    "[| F : transient A; B<=A |] ==> F : transient B"
+    "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
 apply (unfold transient_def, clarify)
 apply (blast intro!: rev_bexI)
 done
 
 lemma transientI: 
-    "[| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> F : transient A"
+    "[| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> F \<in> transient A"
 by (unfold transient_def, blast)
 
 lemma transientE: 
-    "[| F : transient A;   
-        !!act. [| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> P |]  
+    "[| F \<in> transient A;   
+        !!act. [| act: Acts F;  A \<subseteq> Domain act;  act``A \<subseteq> -A |] ==> P |]  
      ==> P"
 by (unfold transient_def, blast)
 
@@ -85,23 +85,23 @@
 subsection{*ensures*}
 
 lemma ensuresI: 
-    "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
+    "[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B"
 by (unfold ensures_def, blast)
 
 lemma ensuresD: 
-    "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
+    "F \<in> A ensures B ==> F \<in> (A-B) co (A \<union> B) & F \<in> transient (A-B)"
 by (unfold ensures_def, blast)
 
 lemma ensures_weaken_R: 
-    "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
+    "[| F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'"
 apply (unfold ensures_def)
 apply (blast intro: constrains_weaken transient_strengthen)
 done
 
 (*The L-version (precondition strengthening) fails, but we have this*)
 lemma stable_ensures_Int: 
-    "[| F : stable C;  F : A ensures B |]    
-    ==> F : (C Int A) ensures (C Int B)"
+    "[| F \<in> stable C;  F \<in> A ensures B |]    
+    ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
 apply (unfold ensures_def)
 apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
 prefer 2 apply (blast intro: transient_strengthen)
@@ -109,78 +109,78 @@
 done
 
 lemma stable_transient_ensures:
-     "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B"
+     "[| F \<in> stable A;  F \<in> transient C;  A \<subseteq> B \<union> C |] ==> F \<in> A ensures B"
 apply (simp add: ensures_def stable_def)
 apply (blast intro: constrains_weaken transient_strengthen)
 done
 
-lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
+lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)"
 by (simp (no_asm) add: ensures_def unless_def)
 
 
 subsection{*leadsTo*}
 
-lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
+lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B"
 apply (unfold leadsTo_def)
 apply (blast intro: leads.Basis)
 done
 
 lemma leadsTo_Trans: 
-     "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C"
+     "[| F \<in> A leadsTo B;  F \<in> B leadsTo C |] ==> F \<in> A leadsTo C"
 apply (unfold leadsTo_def)
 apply (blast intro: leads.Trans)
 done
 
-lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"
+lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
 by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
 
 (*Useful with cancellation, disjunction*)
-lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"
+lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
 by (simp add: Un_ac)
 
 lemma leadsTo_Un_duplicate2:
-     "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"
+     "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
 by (simp add: Un_ac)
 
 (*The Union introduction rule as we should have liked to state it*)
 lemma leadsTo_Union: 
-    "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
+    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
 apply (unfold leadsTo_def)
 apply (blast intro: leads.Union)
 done
 
 lemma leadsTo_Union_Int: 
- "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
 apply (unfold leadsTo_def)
 apply (simp only: Int_Union_Union)
 apply (blast intro: leads.Union)
 done
 
 lemma leadsTo_UN: 
-    "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
+    "(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B"
 apply (subst Union_image_eq [symmetric])
 apply (blast intro: leadsTo_Union)
 done
 
 (*Binary union introduction rule*)
 lemma leadsTo_Un:
-     "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
+     "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
 apply (subst Un_eq_Union)
 apply (blast intro: leadsTo_Union)
 done
 
 lemma single_leadsTo_I: 
-     "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
+     "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
 by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
 
 
 (*The INDUCTION rule as we should have liked to state it*)
 lemma leadsTo_induct: 
-  "[| F : za leadsTo zb;   
-      !!A B. F : A ensures B ==> P A B;  
-      !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]  
+  "[| F \<in> za leadsTo zb;   
+      !!A B. F \<in> A ensures B ==> P A B;  
+      !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]  
                ==> P A C;  
-      !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B  
+      !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B  
    |] ==> P za zb"
 apply (unfold leadsTo_def)
 apply (drule CollectD, erule leads.induct)
@@ -188,7 +188,7 @@
 done
 
 
-lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
+lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
 by (unfold ensures_def constrains_def transient_def, blast)
 
 lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
@@ -205,10 +205,10 @@
 
 (*Lemma is the weak version: can't see how to do it in one step*)
 lemma leadsTo_induct_pre_lemma: 
-  "[| F : za leadsTo zb;   
+  "[| F \<in> za leadsTo zb;   
       P zb;  
-      !!A B. [| F : A ensures B;  P B |] ==> P A;  
-      !!S. ALL A:S. P A ==> P (Union S)  
+      !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
+      !!S. \<forall>A \<in> S. P A ==> P (Union S)  
    |] ==> P za"
 (*by induction on this formula*)
 apply (subgoal_tac "P zb --> P za")
@@ -219,12 +219,12 @@
 done
 
 lemma leadsTo_induct_pre: 
-  "[| F : za leadsTo zb;   
+  "[| F \<in> za leadsTo zb;   
       P zb;  
-      !!A B. [| F : A ensures B;  F : B leadsTo zb;  P B |] ==> P A;  
-      !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)  
+      !!A B. [| F \<in> A ensures B;  F \<in> B leadsTo zb;  P B |] ==> P A;  
+      !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)  
    |] ==> P za"
-apply (subgoal_tac "F : za leadsTo zb & P za")
+apply (subgoal_tac "F \<in> za leadsTo zb & P za")
 apply (erule conjunct2)
 apply (erule leadsTo_induct_pre_lemma)
 prefer 3 apply (blast intro: leadsTo_Union)
@@ -233,76 +233,76 @@
 done
 
 
-lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
+lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
 by (blast intro: subset_imp_leadsTo leadsTo_Trans)
 
 lemma leadsTo_weaken_L [rule_format]:
-     "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
+     "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
 by (blast intro: leadsTo_Trans subset_imp_leadsTo)
 
 (*Distributes over binary unions*)
 lemma leadsTo_Un_distrib:
-     "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)"
+     "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
 by (blast intro: leadsTo_Un leadsTo_weaken_L)
 
 lemma leadsTo_UN_distrib:
-     "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)"
+     "F \<in> (\<Union>i \<in> I. A i) leadsTo B  =  (\<forall>i \<in> I. F \<in> (A i) leadsTo B)"
 by (blast intro: leadsTo_UN leadsTo_weaken_L)
 
 lemma leadsTo_Union_distrib:
-     "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)"
+     "F \<in> (Union S) leadsTo B  =  (\<forall>A \<in> S. F \<in> A leadsTo B)"
 by (blast intro: leadsTo_Union leadsTo_weaken_L)
 
 
 lemma leadsTo_weaken:
-     "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"
+     "[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'"
 by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
 
 
 (*Set difference: maybe combine with leadsTo_weaken_L?*)
 lemma leadsTo_Diff:
-     "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C"
+     "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
 by (blast intro: leadsTo_Un leadsTo_weaken)
 
 lemma leadsTo_UN_UN:
-   "(!! i. i:I ==> F : (A i) leadsTo (A' i))  
-    ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
+   "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))  
+    ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
 apply (simp only: Union_image_eq [symmetric])
 apply (blast intro: leadsTo_Union leadsTo_weaken_R)
 done
 
 (*Binary union version*)
 lemma leadsTo_Un_Un:
-     "[| F : A leadsTo A'; F : B leadsTo B' |]  
-      ==> F : (A Un B) leadsTo (A' Un B')"
+     "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]  
+      ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
 by (blast intro: leadsTo_Un leadsTo_weaken_R)
 
 
 (** The cancellation law **)
 
 lemma leadsTo_cancel2:
-     "[| F : A leadsTo (A' Un B); F : B leadsTo B' |]  
-      ==> F : A leadsTo (A' Un B')"
+     "[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |]  
+      ==> F \<in> A leadsTo (A' \<union> B')"
 by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
 
 lemma leadsTo_cancel_Diff2:
-     "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]  
-      ==> F : A leadsTo (A' Un B')"
+     "[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |]  
+      ==> F \<in> A leadsTo (A' \<union> B')"
 apply (rule leadsTo_cancel2)
 prefer 2 apply assumption
 apply (simp_all (no_asm_simp))
 done
 
 lemma leadsTo_cancel1:
-     "[| F : A leadsTo (B Un A'); F : B leadsTo B' |]  
-    ==> F : A leadsTo (B' Un A')"
+     "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |]  
+    ==> F \<in> A leadsTo (B' \<union> A')"
 apply (simp add: Un_commute)
 apply (blast intro!: leadsTo_cancel2)
 done
 
 lemma leadsTo_cancel_Diff1:
-     "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]  
-    ==> F : A leadsTo (B' Un A')"
+     "[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |]  
+    ==> F \<in> A leadsTo (B' \<union> A')"
 apply (rule leadsTo_cancel1)
 prefer 2 apply assumption
 apply (simp_all (no_asm_simp))
@@ -312,7 +312,7 @@
 
 (** The impossibility law **)
 
-lemma leadsTo_empty: "F : A leadsTo {} ==> A={}"
+lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}"
 apply (erule leadsTo_induct_pre)
 apply (simp_all add: ensures_def constrains_def transient_def, blast)
 done
@@ -322,8 +322,8 @@
 
 (*Special case of PSP: Misra's "stable conjunction"*)
 lemma psp_stable: 
-   "[| F : A leadsTo A'; F : stable B |]  
-    ==> F : (A Int B) leadsTo (A' Int B)"
+   "[| F \<in> A leadsTo A'; F \<in> stable B |]  
+    ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
 apply (unfold stable_def)
 apply (erule leadsTo_induct)
 prefer 3 apply (blast intro: leadsTo_Union_Int)
@@ -334,19 +334,19 @@
 done
 
 lemma psp_stable2: 
-   "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"
+   "[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')"
 by (simp add: psp_stable Int_ac)
 
 lemma psp_ensures: 
-   "[| F : A ensures A'; F : B co B' |]  
-    ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
+   "[| F \<in> A ensures A'; F \<in> B co B' |]  
+    ==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
 apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
 apply (blast intro: transient_strengthen)
 done
 
 lemma psp:
-     "[| F : A leadsTo A'; F : B co B' |]  
-      ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
+     "[| F \<in> A leadsTo A'; F \<in> B co B' |]  
+      ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
 apply (erule leadsTo_induct)
   prefer 3 apply (blast intro: leadsTo_Union_Int)
  txt{*Basis case*}
@@ -359,13 +359,13 @@
 done
 
 lemma psp2:
-     "[| F : A leadsTo A'; F : B co B' |]  
-    ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"
+     "[| F \<in> A leadsTo A'; F \<in> B co B' |]  
+    ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
 by (simp (no_asm_simp) add: psp Int_ac)
 
 lemma psp_unless: 
-   "[| F : A leadsTo A';  F : B unless B' |]  
-    ==> F : (A Int B) leadsTo ((A' Int B) Un B')"
+   "[| F \<in> A leadsTo A';  F \<in> B unless B' |]  
+    ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
 
 apply (unfold unless_def)
 apply (drule psp, assumption)
@@ -379,11 +379,11 @@
 
 lemma leadsTo_wf_induct_lemma:
      "[| wf r;      
-         ALL m. F : (A Int f-`{m}) leadsTo                      
-                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
-      ==> F : (A Int f-`{m}) leadsTo B"
+         \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
+                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+      ==> F \<in> (A \<inter> f-`{m}) leadsTo B"
 apply (erule_tac a = m in wf_induct)
-apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
+apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B")
  apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
 apply (subst vimage_eq_UN)
 apply (simp only: UN_simps [symmetric])
@@ -394,9 +394,9 @@
 (** Meta or object quantifier ? **)
 lemma leadsTo_wf_induct:
      "[| wf r;      
-         ALL m. F : (A Int f-`{m}) leadsTo                      
-                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
-      ==> F : A leadsTo B"
+         \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo                      
+                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+      ==> F \<in> A leadsTo B"
 apply (rule_tac t = A in subst)
  defer 1
  apply (rule leadsTo_UN)
@@ -408,102 +408,102 @@
 
 lemma bounded_induct:
      "[| wf r;      
-         ALL m:I. F : (A Int f-`{m}) leadsTo                    
-                      ((A Int f-`(r^-1 `` {m})) Un B) |]  
-      ==> F : A leadsTo ((A - (f-`I)) Un B)"
+         \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo                    
+                      ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
+      ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)"
 apply (erule leadsTo_wf_induct, safe)
-apply (case_tac "m:I")
+apply (case_tac "m \<in> I")
 apply (blast intro: leadsTo_weaken)
 apply (blast intro: subset_imp_leadsTo)
 done
 
 
-(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
+(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
 lemma lessThan_induct: 
-     "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]  
-      ==> F : A leadsTo B"
+     "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..m(}) \<union> B) |]  
+      ==> F \<in> A leadsTo B"
 apply (rule wf_less_than [THEN leadsTo_wf_induct])
 apply (simp (no_asm_simp))
 apply blast
 done
 
 lemma lessThan_bounded_induct:
-     "!!l::nat. [| ALL m:(greaterThan l).     
-            F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]  
-      ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
+     "!!l::nat. [| \<forall>m \<in> greaterThan l.     
+            F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |]  
+      ==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
 apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
 apply (rule wf_less_than [THEN bounded_induct])
 apply (simp (no_asm_simp))
 done
 
 lemma greaterThan_bounded_induct:
-     "!!l::nat. [| ALL m:(lessThan l).     
-            F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]  
-      ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
+     "(!!l::nat. \<forall>m \<in> lessThan l.     
+                 F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B))
+      ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
 apply (rule_tac f = f and f1 = "%k. l - k" 
        in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
 apply (simp (no_asm) add: inv_image_def Image_singleton)
 apply clarify
 apply (case_tac "m<l")
-prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
-apply (blast intro: leadsTo_weaken_R diff_less_mono2)
+ apply (blast intro: leadsTo_weaken_R diff_less_mono2)
+apply (blast intro: not_leE subset_imp_leadsTo)
 done
 
 
 subsection{*wlt*}
 
 (*Misra's property W3*)
-lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
+lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
 apply (unfold wlt_def)
 apply (blast intro!: leadsTo_Union)
 done
 
-lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
+lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B"
 apply (unfold wlt_def)
 apply (blast intro!: leadsTo_Union)
 done
 
 (*Misra's property W2*)
-lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"
+lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
 by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
 
 (*Misra's property W4*)
-lemma wlt_increasing: "B <= wlt F B"
+lemma wlt_increasing: "B \<subseteq> wlt F B"
 apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
 done
 
 
 (*Used in the Trans case below*)
 lemma lemma1: 
-   "[| B <= A2;   
-       F : (A1 - B) co (A1 Un B);  
-       F : (A2 - C) co (A2 Un C) |]  
-    ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
+   "[| B \<subseteq> A2;   
+       F \<in> (A1 - B) co (A1 \<union> B);  
+       F \<in> (A2 - C) co (A2 \<union> C) |]  
+    ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
 by (unfold constrains_def, clarify,  blast)
 
 (*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
 lemma leadsTo_123:
-     "F : A leadsTo A'  
-      ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
+     "F \<in> A leadsTo A'  
+      ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
 apply (erule leadsTo_induct)
 (*Basis*)
 apply (blast dest: ensuresD)
 (*Trans*)
 apply clarify
-apply (rule_tac x = "Ba Un Bb" in exI)
+apply (rule_tac x = "Ba \<union> Bb" in exI)
 apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
 (*Union*)
 apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
-apply (rule_tac x = "UN A:S. f A" in exI)
+apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
 apply (auto intro: leadsTo_UN)
 (*Blast_tac says PROOF FAILED*)
-apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" 
+apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B" 
        in constrains_UN [THEN constrains_weaken], auto) 
 done
 
 
 (*Misra's property W5*)
-lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
+lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
 proof -
   from wlt_leadsTo [of F B, THEN leadsTo_123]
   show ?thesis
@@ -527,28 +527,28 @@
 subsection{*Completion: Binary and General Finite versions*}
 
 lemma completion_lemma :
-     "[| W = wlt F (B' Un C);      
-       F : A leadsTo (A' Un C);  F : A' co (A' Un C);    
-       F : B leadsTo (B' Un C);  F : B' co (B' Un C) |]  
-    ==> F : (A Int B) leadsTo ((A' Int B') Un C)"
-apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
+     "[| W = wlt F (B' \<union> C);      
+       F \<in> A leadsTo (A' \<union> C);  F \<in> A' co (A' \<union> C);    
+       F \<in> B leadsTo (B' \<union> C);  F \<in> B' co (B' \<union> C) |]  
+    ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
+apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ")
  prefer 2
  apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 
                                          THEN constrains_weaken])
-apply (subgoal_tac "F : (W-C) co W")
+apply (subgoal_tac "F \<in> (W-C) co W")
  prefer 2
  apply (simp add: wlt_increasing Un_assoc Un_absorb2)
-apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
+apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
  prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
 (** LEVEL 6 **)
-apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
+apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
  prefer 2
  apply (rule leadsTo_Un_duplicate2)
  apply (blast intro: leadsTo_Un_Un wlt_leadsTo
                          [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
 apply (drule leadsTo_Diff)
 apply (blast intro: subset_imp_leadsTo)
-apply (subgoal_tac "A Int B <= A Int W")
+apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")
  prefer 2
  apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
 apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
@@ -557,9 +557,9 @@
 lemmas completion = completion_lemma [OF refl]
 
 lemma finite_completion_lemma:
-     "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->   
-                   (ALL i:I. F : (A' i) co (A' i Un C)) -->  
-                   F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+     "finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) -->   
+                   (\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) -->  
+                   F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
 apply (erule finite_induct, auto)
 apply (rule completion)
    prefer 4
@@ -569,15 +569,15 @@
 
 lemma finite_completion: 
      "[| finite I;   
-         !!i. i:I ==> F : (A i) leadsTo (A' i Un C);  
-         !!i. i:I ==> F : (A' i) co (A' i Un C) |]    
-      ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+         !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C);  
+         !!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |]    
+      ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
 by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
 
 lemma stable_completion: 
-     "[| F : A leadsTo A';  F : stable A';    
-         F : B leadsTo B';  F : stable B' |]  
-    ==> F : (A Int B) leadsTo (A' Int B')"
+     "[| F \<in> A leadsTo A';  F \<in> stable A';    
+         F \<in> B leadsTo B';  F \<in> stable B' |]  
+    ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
 apply (unfold stable_def)
 apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
 apply (force+)
@@ -585,9 +585,9 @@
 
 lemma finite_stable_completion: 
      "[| finite I;   
-         !!i. i:I ==> F : (A i) leadsTo (A' i);  
-         !!i. i:I ==> F : stable (A' i) |]    
-      ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
+         !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i);  
+         !!i. i \<in> I ==> F \<in> stable (A' i) |]    
+      ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)"
 apply (unfold stable_def)
 apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
 apply (simp_all (no_asm_simp))