# HG changeset patch
# User paulson
# Date 1044448532 -3600
# Node ID fd40c9d9076bc17e05077624f2481b7b728922b8
# Parent  3786b2fd680800c64032056fff8b5aea71b55384
more tidying

diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Channel.thy
--- a/src/HOL/UNITY/Simple/Channel.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -17,19 +17,19 @@
 
 constdefs
   minSet :: "nat set => nat option"
-    "minSet A == if A={} then None else Some (LEAST x. x:A)"
+    "minSet A == if A={} then None else Some (LEAST x. x \<in> A)"
 
 axioms
 
-  UC1:  "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
+  UC1:  "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
 
-  (*  UC1  "F : {s. minSet s = x} co {s. x <= minSet s}"  *)
+  (*  UC1  "F \<in> {s. minSet s = x} co {s. x \<subseteq> minSet s}"  *)
 
-  UC2:  "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
+  UC2:  "F \<in> (minSet -` {Some x}) leadsTo {s. x \<notin> s}"
 
 
 (*None represents "infinity" while Some represents proper integers*)
-lemma minSet_eq_SomeD: "minSet A = Some x ==> x : A"
+lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A"
 apply (unfold minSet_def)
 apply (simp split: split_if_asm)
 apply (fast intro: LeastI)
@@ -38,11 +38,11 @@
 lemma minSet_empty [simp]: " minSet{} = None"
 by (unfold minSet_def, simp)
 
-lemma minSet_nonempty: "x:A ==> minSet A = Some (LEAST x. x: A)"
+lemma minSet_nonempty: "x \<in> A ==> minSet A = Some (LEAST x. x \<in> A)"
 by (unfold minSet_def, auto)
 
 lemma minSet_greaterThan:
-     "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
+     "F \<in> (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
 apply (rule leadsTo_weaken)
 apply (rule_tac x1=x in psp [OF UC2 UC1], safe)
 apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff)
@@ -50,7 +50,7 @@
 
 (*The induction*)
 lemma Channel_progress_lemma:
-     "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
+     "F \<in> (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac l = y and f = "the o minSet" and B = "{}" 
        in greaterThan_bounded_induct, safe)
@@ -63,7 +63,7 @@
 done
 
 
-lemma Channel_progress: "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"
+lemma Channel_progress: "!!y::nat. F \<in> (UNIV-{{}}) leadsTo {s. y \<notin> s}"
 apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify)
 apply (frule minSet_nonempty)
 apply (auto dest: Suc_le_lessD not_less_Least)
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -17,56 +17,56 @@
   gtime :: "nat=>nat"
 
 axioms
-  fmono: "m <= n ==> ftime m <= ftime n"
-  gmono: "m <= n ==> gtime m <= gtime n"
+  fmono: "m \<le> n ==> ftime m \<le> ftime n"
+  gmono: "m \<le> n ==> gtime m \<le> gtime n"
 
-  fasc:  "m <= ftime n"
-  gasc:  "m <= gtime n"
+  fasc:  "m \<le> ftime n"
+  gasc:  "m \<le> gtime n"
 
 constdefs
   common :: "nat set"
     "common == {n. ftime n = n & gtime n = n}"
 
   maxfg :: "nat => nat set"
-    "maxfg m == {t. t <= max (ftime m) (gtime m)}"
+    "maxfg m == {t. t \<le> max (ftime m) (gtime m)}"
 
 
 (*Misra's property CMT4: t exceeds no common meeting time*)
 lemma common_stable:
-     "[| ALL m. F : {m} Co (maxfg m); n: common |]  
-      ==> F : Stable (atMost n)"
-apply (drule_tac M = "{t. t<=n}" in Elimination_sing)
+     "[| \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]  
+      ==> F \<in> Stable (atMost n)"
+apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing)
 apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
 apply (erule Constrains_weaken_R)
 apply (blast intro: order_eq_refl fmono gmono le_trans)
 done
 
 lemma common_safety:
-     "[| Init F <= atMost n;   
-         ALL m. F : {m} Co (maxfg m); n: common |]  
-      ==> F : Always (atMost n)"
+     "[| Init F \<subseteq> atMost n;   
+         \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]  
+      ==> F \<in> Always (atMost n)"
 by (simp add: AlwaysI common_stable)
 
 
 (*** Some programs that implement the safety property above ***)
 
-lemma "SKIP : {m} co (maxfg m)"
+lemma "SKIP \<in> {m} co (maxfg m)"
 by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
 
 (*This one is  t := ftime t || t := gtime t*)
 lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV)
-       : {m} co (maxfg m)"
+       \<in> {m} co (maxfg m)"
 by (simp add: constrains_def maxfg_def le_max_iff_disj fasc)
 
 (*This one is  t := max (ftime t) (gtime t)*)
 lemma  "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)  
-       : {m} co (maxfg m)"
+       \<in> {m} co (maxfg m)"
 by (simp add: constrains_def maxfg_def max_def gasc)
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
 lemma  "mk_program   
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
-       : {m} co (maxfg m)"
+       \<in> {m} co (maxfg m)"
 by (simp add: constrains_def maxfg_def max_def gasc)
 
 
@@ -79,10 +79,10 @@
 declare atMost_Int_atLeast [simp]
 
 lemma leadsTo_common_lemma:
-     "[| ALL m. F : {m} Co (maxfg m);  
-         ALL m: lessThan n. F : {m} LeadsTo (greaterThan m);  
-         n: common |]   
-      ==> F : (atMost n) LeadsTo common"
+     "[| \<forall>m. F \<in> {m} Co (maxfg m);  
+         \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);  
+         n \<in> common |]   
+      ==> F \<in> (atMost n) LeadsTo common"
 apply (rule LeadsTo_weaken_R)
 apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
 apply (simp_all (no_asm_simp))
@@ -90,12 +90,12 @@
 apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
 done
 
-(*The "ALL m: -common" form echoes CMT6.*)
+(*The "\<forall>m \<in> -common" form echoes CMT6.*)
 lemma leadsTo_common:
-     "[| ALL m. F : {m} Co (maxfg m);  
-         ALL m: -common. F : {m} LeadsTo (greaterThan m);  
-         n: common |]   
-      ==> F : (atMost (LEAST n. n: common)) LeadsTo common"
+     "[| \<forall>m. F \<in> {m} Co (maxfg m);  
+         \<forall>m \<in> -common. F \<in> {m} LeadsTo (greaterThan m);  
+         n \<in> common |]   
+      ==> F \<in> (atMost (LEAST n. n \<in> common)) LeadsTo common"
 apply (rule leadsTo_common_lemma)
 apply (simp_all (no_asm_simp))
 apply (erule_tac [2] LeastI)
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Deadlock.thy
--- a/src/HOL/UNITY/Simple/Deadlock.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Deadlock.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -10,66 +10,61 @@
 theory Deadlock = UNITY:
 
 (*Trivial, two-process case*)
-lemma "[| F : (A Int B) co A;  F : (B Int A) co B |] ==> F : stable (A Int B)"
+lemma "[| F \<in> (A \<inter> B) co A;  F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)"
 by (unfold constrains_def stable_def, blast)
 
 
 (*a simplification step*)
 lemma Collect_le_Int_equals:
-     "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"
+     "(\<Inter>i \<in> atMost n. A(Suc i) \<inter> A i) = (\<Inter>i \<in> atMost (Suc n). A i)"
 apply (induct_tac "n")
-apply (simp_all (no_asm_simp) add: atMost_Suc)
-apply auto
+apply (auto simp add: atMost_Suc)
 done
 
 (*Dual of the required property.  Converse inclusion fails.*)
 lemma UN_Int_Compl_subset:
-     "(UN i: lessThan n. A i) Int (- A n) <=   
-      (UN i: lessThan n. (A i) Int (- A (Suc i)))"
-apply (induct_tac "n")
-apply (simp (no_asm_simp))
-apply (simp (no_asm) add: lessThan_Suc)
-apply blast
+     "(\<Union>i \<in> lessThan n. A i) \<inter> (- A n) \<subseteq>   
+      (\<Union>i \<in> lessThan n. (A i) \<inter> (- A (Suc i)))"
+apply (induct_tac "n", simp)
+apply (simp add: lessThan_Suc, blast)
 done
 
 
 (*Converse inclusion fails.*)
 lemma INT_Un_Compl_subset:
-     "(INT i: lessThan n. -A i Un A (Suc i))  <=  
-      (INT i: lessThan n. -A i) Un A n"
-apply (induct_tac "n")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp) add: lessThan_Suc)
-apply blast
+     "(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i))  \<subseteq>  
+      (\<Inter>i \<in> lessThan n. -A i) \<union> A n"
+apply (induct_tac "n", simp)
+apply (simp add: lessThan_Suc, blast)
 done
 
 
 (*Specialized rewriting*)
 lemma INT_le_equals_Int_lemma:
-     "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}"
+     "A 0 \<inter> (-(A n) \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i))) = {}"
 by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD])
 
 (*Reverse direction makes it harder to invoke the ind hyp*)
 lemma INT_le_equals_Int:
-     "(INT i: atMost n. A i) =  
-      A 0 Int (INT i: lessThan n. -A i Un A(Suc i))"
+     "(\<Inter>i \<in> atMost n. A i) =  
+      A 0 \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A(Suc i))"
 apply (induct_tac "n", simp)
 apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2
                  INT_le_equals_Int_lemma lessThan_Suc atMost_Suc)
 done
 
 lemma INT_le_Suc_equals_Int:
-     "(INT i: atMost (Suc n). A i) =  
-      A 0 Int (INT i: atMost n. -A i Un A(Suc i))"
+     "(\<Inter>i \<in> atMost (Suc n). A i) =  
+      A 0 \<inter> (\<Inter>i \<in> atMost n. -A i \<union> A(Suc i))"
 by (simp add: lessThan_Suc_atMost INT_le_equals_Int)
 
 
 (*The final deadlock example*)
 lemma
-  assumes zeroprem: "F : (A 0 Int A (Suc n)) co (A 0)"
+  assumes zeroprem: "F \<in> (A 0 \<inter> A (Suc n)) co (A 0)"
       and allprem:
-	    "!!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i))"
-  shows "F : stable (INT i: atMost (Suc n). A i)"
+	    "!!i. i \<in> atMost n ==> F \<in> (A(Suc i) \<inter> A i) co (-A i \<union> A(Suc i))"
+  shows "F \<in> stable (\<Inter>i \<in> atMost (Suc n). A i)"
 apply (unfold stable_def) 
 apply (rule constrains_Int [THEN constrains_weaken])
    apply (rule zeroprem) 
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -21,26 +21,26 @@
   Max :: "int"       (*least and greatest floors*)
 
 axioms
-  Min_le_Max [iff]: "Min <= Max"
+  Min_le_Max [iff]: "Min \<le> Max"
   
 constdefs
   
   (** Abbreviations: the "always" part **)
   
   above :: "state set"
-    "above == {s. EX i. floor s < i & i <= Max & i : req s}"
+    "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
 
   below :: "state set"
-    "below == {s. EX i. Min <= i & i < floor s & i : req s}"
+    "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
 
   queueing :: "state set"
-    "queueing == above Un below"
+    "queueing == above \<union> below"
 
   goingup :: "state set"
-    "goingup   == above Int  ({s. up s}  Un -below)"
+    "goingup   == above \<inter> ({s. up s}  \<union> -below)"
 
   goingdown :: "state set"
-    "goingdown == below Int ({s. ~ up s} Un -above)"
+    "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
 
   ready :: "state set"
     "ready == {s. stop s & ~ open s & move s}"
@@ -63,7 +63,7 @@
     "atFloor n ==  {s. floor s = n}"
 
   Req :: "int => state set"
-    "Req n ==  {s. n : req s}"
+    "Req n ==  {s. n \<in> req s}"
 
 
   
@@ -71,15 +71,15 @@
   
   request_act :: "(state*state) set"
     "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
-		                  & ~ stop s & floor s : req s}"
+		                  & ~ stop s & floor s \<in> req s}"
 
   open_act :: "(state*state) set"
     "open_act ==
          {(s,s'). s' = s (|open :=True,
 			   req  := req s - {floor s},
 			   move := True|)
-		       & stop s & ~ open s & floor s : req s
-	               & ~(move s & s: queueing)}"
+		       & stop s & ~ open s & floor s \<in> req s
+	               & ~(move s & s \<in> queueing)}"
 
   close_act :: "(state*state) set"
     "close_act == {(s,s'). s' = s (|open := False|) & open s}"
@@ -89,24 +89,24 @@
          {(s,s'). s' = s (|stop  :=False,
 			   floor := floor s + 1,
 			   up    := True|)
-		       & s : (ready Int goingup)}"
+		       & s \<in> (ready \<inter> goingup)}"
 
   req_down :: "(state*state) set"
     "req_down ==
          {(s,s'). s' = s (|stop  :=False,
 			   floor := floor s - 1,
 			   up    := False|)
-		       & s : (ready Int goingdown)}"
+		       & s \<in> (ready \<inter> goingdown)}"
 
   move_up :: "(state*state) set"
     "move_up ==
          {(s,s'). s' = s (|floor := floor s + 1|)
-		       & ~ stop s & up s & floor s ~: req s}"
+		       & ~ stop s & up s & floor s \<notin> req s}"
 
   move_down :: "(state*state) set"
     "move_down ==
          {(s,s'). s' = s (|floor := floor s - 1|)
-		       & ~ stop s & ~ up s & floor s ~: req s}"
+		       & ~ stop s & ~ up s & floor s \<notin> req s}"
 
   (*This action is omitted from prior treatments, which therefore are
     unrealistic: nobody asks the lift to do anything!  But adding this
@@ -114,8 +114,8 @@
     "ensures" properties fail.*)
   button_press  :: "(state*state) set"
     "button_press ==
-         {(s,s'). EX n. s' = s (|req := insert n (req s)|)
-		        & Min <= n & n <= Max}"
+         {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
+		        & Min \<le> n & n \<le> Max}"
 
 
   Lift :: "state program"
@@ -130,7 +130,7 @@
   (** Invariants **)
 
   bounded :: "state set"
-    "bounded == {s. Min <= floor s & floor s <= Max}"
+    "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
 
   open_stop :: "state set"
     "open_stop == {s. open s --> stop s}"
@@ -139,15 +139,15 @@
     "open_move == {s. open s --> move s}"
   
   stop_floor :: "state set"
-    "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
+    "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
   
   moving_up :: "state set"
     "moving_up == {s. ~ stop s & up s -->
-                   (EX f. floor s <= f & f <= Max & f : req s)}"
+                   (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
   
   moving_down :: "state set"
     "moving_down == {s. ~ stop s & ~ up s -->
-                     (EX f. Min <= f & f <= floor s & f : req s)}"
+                     (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
   
   metric :: "[int,state] => int"
     "metric ==
@@ -160,10 +160,10 @@
 
 locale Floor =
   fixes n
-  assumes Min_le_n [iff]: "Min <= n"
-      and n_le_Max [iff]: "n <= Max"
+  assumes Min_le_n [iff]: "Min \<le> n"
+      and n_le_Max [iff]: "n \<le> Max"
 
-lemma not_mem_distinct: "[| x ~: A;  y : A |] ==> x ~= y"
+lemma not_mem_distinct: "[| x \<notin> A;  y \<in> A |] ==> x \<noteq> y"
 by blast
 
 
@@ -194,36 +194,36 @@
         moving_up_def [simp]
         moving_down_def [simp]
 
-lemma open_stop: "Lift : Always open_stop"
+lemma open_stop: "Lift \<in> Always open_stop"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains) 
 done
 
-lemma stop_floor: "Lift : Always stop_floor"
+lemma stop_floor: "Lift \<in> Always stop_floor"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 done
 
 (*This one needs open_stop, which was proved above*)
-lemma open_move: "Lift : Always open_move"
+lemma open_move: "Lift \<in> Always open_move"
 apply (cut_tac open_stop)
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 done
 
-lemma moving_up: "Lift : Always moving_up"
+lemma moving_up: "Lift \<in> Always moving_up"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
 done
 
-lemma moving_down: "Lift : Always moving_down"
+lemma moving_down: "Lift \<in> Always moving_down"
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains)
 apply (blast dest: zle_imp_zless_or_eq)
 done
 
-lemma bounded: "Lift : Always bounded"
+lemma bounded: "Lift \<in> Always bounded"
 apply (cut_tac moving_up moving_down)
 apply (rule AlwaysI, force) 
 apply (unfold Lift_def, constrains, auto)
@@ -244,24 +244,24 @@
 (** The HUG'93 paper mistakenly omits the Req n from these! **)
 
 (** Lift_1 **)
-lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"
+lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
 apply (cut_tac stop_floor)
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_5*)
 
-lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo  
-                     (Req n Int opened - atFloor n)"
+lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo  
+                     (Req n \<inter> opened - atFloor n)"
 apply (cut_tac stop_floor)
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_1*)
 
-lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo  
-                     (Req n Int closed - (atFloor n - queueing))"
+lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo  
+                     (Req n \<inter> closed - (atFloor n - queueing))"
 apply (unfold Lift_def, ensures_tac "close_act")
 done  (*lem_lift_1_2*)
 
-lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing))   
-             LeadsTo (opened Int atFloor n)"
+lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))   
+             LeadsTo (opened \<inter> atFloor n)"
 apply (unfold Lift_def, ensures_tac "open_act")
 done  (*lem_lift_1_7*)
 
@@ -283,14 +283,14 @@
   NOT an ensures_tac property, but a mere inclusion
   don't know why script lift_2.uni says ENSURES*)
 lemma (in Floor) E_thm05c: 
-    "Lift : (Req n Int closed - (atFloor n - queueing))    
-             LeadsTo ((closed Int goingup Int Req n)  Un  
-                      (closed Int goingdown Int Req n))"
+    "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
+             LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
+                      (closed \<inter> goingdown \<inter> Req n))"
 by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
 
 (*lift_2*)
-lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing))    
-             LeadsTo (moving Int Req n)"
+lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
+             LeadsTo (moving \<inter> Req n)"
 apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
 apply (unfold Lift_def) 
 apply (ensures_tac [2] "req_down")
@@ -306,13 +306,13 @@
 (*lem_lift_4_1 *)
 lemma (in Floor) E_thm12a:
      "0 < N ==>  
-      Lift : (moving Int Req n Int {s. metric n s = N} Int  
-              {s. floor s ~: req s} Int {s. up s})    
+      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+              {s. floor s \<notin> req s} \<inter> {s. up s})    
              LeadsTo  
-               (moving Int Req n Int {s. metric n s < N})"
+               (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac moving_up)
 apply (unfold Lift_def, ensures_tac "move_up", safe)
-(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
+(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
 apply (erule linorder_leI [THEN order_antisym, symmetric])
 apply (auto simp add: metric_def)
 done
@@ -320,21 +320,21 @@
 
 (*lem_lift_4_3 *)
 lemma (in Floor) E_thm12b: "0 < N ==>  
-      Lift : (moving Int Req n Int {s. metric n s = N} Int  
-              {s. floor s ~: req s} - {s. up s})    
-             LeadsTo (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+              {s. floor s \<notin> req s} - {s. up s})    
+             LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac moving_down)
 apply (unfold Lift_def, ensures_tac "move_down", safe)
-(*this step consolidates two formulae to the goal  metric n s' <= metric n s*)
+(*this step consolidates two formulae to the goal  metric n s' \<le> metric n s*)
 apply (erule linorder_leI [THEN order_antisym, symmetric])
 apply (auto simp add: metric_def)
 done
 
 (*lift_4*)
 lemma (in Floor) lift_4:
-     "0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int  
-                            {s. floor s ~: req s}) LeadsTo      
-                           (moving Int Req n Int {s. metric n s < N})"
+     "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> 
+                            {s. floor s \<notin> req s}) LeadsTo      
+                           (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
                               LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
 done
@@ -344,8 +344,8 @@
 
 (*lem_lift_5_3*)
 lemma (in Floor) E_thm16a: "0<N    
-  ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo  
-             (moving Int Req n Int {s. metric n s < N})"
+  ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo  
+             (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "req_up")
 apply (auto simp add: metric_def)
@@ -354,8 +354,8 @@
 
 (*lem_lift_5_1 has ~goingup instead of goingdown*)
 lemma (in Floor) E_thm16b: "0<N ==>    
-      Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo  
-                   (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo  
+                   (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "req_down")
 apply (auto simp add: metric_def)
@@ -365,14 +365,14 @@
 (*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
   i.e. the trivial disjunction, leading to an asymmetrical proof.*)
 lemma (in Floor) E_thm16c:
-     "0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown"
+     "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> goingdown"
 by (force simp add: metric_def)
 
 
 (*lift_5*)
 lemma (in Floor) lift_5:
-     "0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo    
-                     (moving Int Req n Int {s. metric n s < N})"
+     "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo    
+                     (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
                               LeadsTo_Un [OF E_thm16a E_thm16b]])
 apply (drule E_thm16c, auto)
@@ -383,37 +383,37 @@
 
 (*lemma used to prove lem_lift_3_1*)
 lemma (in Floor) metric_eq_0D [dest]:
-     "[| metric n s = 0;  Min <= floor s;  floor s <= Max |] ==> floor s = n"
+     "[| metric n s = 0;  Min \<le> floor s;  floor s \<le> Max |] ==> floor s = n"
 by (force simp add: metric_def)
 
 
 (*lem_lift_3_1*)
-lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo    
-                       (stopped Int atFloor n)"
+lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo    
+                       (stopped \<inter> atFloor n)"
 apply (cut_tac bounded)
 apply (unfold Lift_def, ensures_tac "request_act", auto)
 done
 
 (*lem_lift_3_5*)
 lemma (in Floor) E_thm13: 
-  "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
-  LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"
+  "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
+  LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})"
 apply (unfold Lift_def, ensures_tac "request_act")
 apply (auto simp add: metric_def)
 done
 
 (*lem_lift_3_6*)
 lemma (in Floor) E_thm14: "0 < N ==>  
-      Lift :  
-        (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})  
-        LeadsTo (opened Int Req n Int {s. metric n s = N})"
+      Lift \<in>  
+        (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})  
+        LeadsTo (opened \<inter> Req n \<inter> {s. metric n s = N})"
 apply (unfold Lift_def, ensures_tac "open_act")
 apply (auto simp add: metric_def)
 done
 
 (*lem_lift_3_7*)
-lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N})   
-             LeadsTo (closed Int Req n Int {s. metric n s = N})"
+lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})   
+             LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
 apply (unfold Lift_def, ensures_tac "close_act")
 apply (auto simp add: metric_def)
 done
@@ -422,15 +422,15 @@
 (** the final steps **)
 
 lemma (in Floor) lift_3_Req: "0 < N ==>  
-      Lift :  
-        (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s})    
-        LeadsTo (moving Int Req n Int {s. metric n s < N})"
+      Lift \<in>  
+        (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})    
+        LeadsTo (moving \<inter> Req n \<inter> {s. metric n s < N})"
 apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans)
 done
 
 
 (*Now we observe that our integer metric is really a natural number*)
-lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}"
+lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
 apply (rule bounded [THEN Always_weaken])
 apply (auto simp add: metric_def)
 done
@@ -438,10 +438,10 @@
 lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11]
 
 lemma (in Floor) lift_3:
-     "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"
+     "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
 apply (rule Always_nonneg [THEN integ_0_le_induct])
 apply (case_tac "0 < z")
-(*If z <= 0 then actually z = 0*)
+(*If z \<le> 0 then actually z = 0*)
 prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less)
 apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1])
 apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
@@ -449,7 +449,7 @@
 done
 
 
-lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
+lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
 apply (rule LeadsTo_Trans)
  prefer 2
  apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Mutex.thy
--- a/src/HOL/UNITY/Simple/Mutex.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Mutex.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -62,16 +62,16 @@
   (** The correct invariants **)
 
   IU :: "state set"
-    "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
+    "IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
 
   IV :: "state set"
-    "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
+    "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
 
   (** The faulty invariant (for U alone) **)
 
   bad_IU :: "state set"
-    "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
-	           (3 <= m s & m s <= 4 --> ~ p s)}"
+    "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) &
+	           (3 \<le> m s & m s \<le> 4 --> ~ p s)}"
 
 
 declare Mutex_def [THEN def_prg_Init, simp]
@@ -91,26 +91,26 @@
 declare IV_def [THEN def_set_simp, simp]
 declare bad_IU_def [THEN def_set_simp, simp]
 
-lemma IU: "Mutex : Always IU"
+lemma IU: "Mutex \<in> Always IU"
 apply (rule AlwaysI, force) 
 apply (unfold Mutex_def, constrains) 
 done
 
 
-lemma IV: "Mutex : Always IV"
+lemma IV: "Mutex \<in> Always IV"
 apply (rule AlwaysI, force) 
 apply (unfold Mutex_def, constrains)
 done
 
 (*The safety property: mutual exclusion*)
-lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"
+lemma mutual_exclusion: "Mutex \<in> Always {s. ~ (m s = 3 & n s = 3)}"
 apply (rule Always_weaken) 
 apply (rule Always_Int_I [OF IU IV], auto)
 done
 
 
 (*The bad invariant FAILS in V1*)
-lemma "Mutex : Always bad_IU"
+lemma "Mutex \<in> Always bad_IU"
 apply (rule AlwaysI, force) 
 apply (unfold Mutex_def, constrains, auto)
 (*Resulting state: n=1, p=false, m=4, u=false.  
@@ -119,90 +119,90 @@
 oops
 
 
-lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
+lemma eq_123: "((1::int) \<le> i & i \<le> 3) = (i = 1 | i = 2 | i = 3)"
 by arith
 
 
 (*** Progress for U ***)
 
-lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}"
+lemma U_F0: "Mutex \<in> {s. m s=2} Unless {s. m s=3}"
 by (unfold Unless_def Mutex_def, constrains)
 
-lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
-by (unfold Mutex_def, ensures_tac "U1")
+lemma U_F1: "Mutex \<in> {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"
+by (unfold Mutex_def, ensures_tac U1)
 
-lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
+lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
 apply (cut_tac IU)
 apply (unfold Mutex_def, ensures_tac U2)
 done
 
-lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}"
+lemma U_F3: "Mutex \<in> {s. m s = 3} LeadsTo {s. p s}"
 apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans)
  apply (unfold Mutex_def)
  apply (ensures_tac U3)
 apply (ensures_tac U4)
 done
 
-lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}"
+lemma U_lemma2: "Mutex \<in> {s. m s = 2} LeadsTo {s. p s}"
 apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
                              Int_lower2 [THEN subset_imp_LeadsTo]])
 apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto)
 done
 
-lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}"
+lemma U_lemma1: "Mutex \<in> {s. m s = 1} LeadsTo {s. p s}"
 by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast)
 
-lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"
+lemma U_lemma123: "Mutex \<in> {s. 1 \<le> m s & m s \<le> 3} LeadsTo {s. p s}"
 by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3)
 
 (*Misra's F4*)
-lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}"
+lemma u_Leadsto_p: "Mutex \<in> {s. u s} LeadsTo {s. p s}"
 by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto)
 
 
 (*** Progress for V ***)
 
 
-lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}"
+lemma V_F0: "Mutex \<in> {s. n s=2} Unless {s. n s=3}"
 by (unfold Unless_def Mutex_def, constrains)
 
-lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
+lemma V_F1: "Mutex \<in> {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"
 by (unfold Mutex_def, ensures_tac "V1")
 
-lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"
+lemma V_F2: "Mutex \<in> {s. p s & n s = 2} LeadsTo {s. n s = 3}"
 apply (cut_tac IV)
 apply (unfold Mutex_def, ensures_tac "V2")
 done
 
-lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"
+lemma V_F3: "Mutex \<in> {s. n s = 3} LeadsTo {s. ~ p s}"
 apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans)
  apply (unfold Mutex_def)
  apply (ensures_tac V3)
 apply (ensures_tac V4)
 done
 
-lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"
+lemma V_lemma2: "Mutex \<in> {s. n s = 2} LeadsTo {s. ~ p s}"
 apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L
                              Int_lower2 [THEN subset_imp_LeadsTo]])
 apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) 
 done
 
-lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"
+lemma V_lemma1: "Mutex \<in> {s. n s = 1} LeadsTo {s. ~ p s}"
 by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast)
 
-lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"
+lemma V_lemma123: "Mutex \<in> {s. 1 \<le> n s & n s \<le> 3} LeadsTo {s. ~ p s}"
 by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3)
 
 
 (*Misra's F4*)
-lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}"
+lemma v_Leadsto_not_p: "Mutex \<in> {s. v s} LeadsTo {s. ~ p s}"
 by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto)
 
 
 (** Absence of starvation **)
 
 (*Misra's F6*)
-lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"
+lemma m1_Leadsto_3: "Mutex \<in> {s. m s = 1} LeadsTo {s. m s = 3}"
 apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
 apply (rule_tac [2] U_F2)
 apply (simp add: Collect_conj_eq)
@@ -213,7 +213,7 @@
 done
 
 (*The same for V*)
-lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"
+lemma n1_Leadsto_3: "Mutex \<in> {s. n s = 1} LeadsTo {s. n s = 3}"
 apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate])
 apply (rule_tac [2] V_F2)
 apply (simp add: Collect_conj_eq)
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Network.thy
--- a/src/HOL/UNITY/Simple/Network.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Network.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -20,13 +20,13 @@
 
 locale F_props =
   fixes F 
-  assumes rsA: "F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}"
-      and rsB: "F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}"
-    and sent_nondec: "F : stable {s. m <= s(proc,Sent)}"
-    and rcvd_nondec: "F : stable {s. n <= s(proc,Rcvd)}"
-    and rcvd_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
+  assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}"
+      and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}"
+    and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}"
+    and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}"
+    and rcvd_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m}
                         co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}"
-    and sent_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
+    and sent_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
                         co {s. s(proc,Sent) = n}"
   
 
@@ -51,7 +51,7 @@
                                          idle_AB]
 
 lemma (in F_props)
-  shows "F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &  
+  shows "F \<in> stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &  
 			s(Aproc,Sent) = s(Bproc,Rcvd) &  
 			s(Bproc,Sent) = s(Aproc,Rcvd) &  
 			s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"
@@ -60,7 +60,7 @@
 apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, 
                              THEN constrainsD], assumption)
 apply simp_all
-apply (blast intro!: order_refl del: le0, clarify) 
+apply (blast del: le0, clarify) 
 apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
 apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") 
 apply simp 
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -24,13 +24,13 @@
     "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
 
   Rprg :: "state program"
-    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
+    "Rprg == mk_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
 
   reach_invariant :: "state set"
-    "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+    "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
 
   fixedpoint :: "state set"
-    "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
+    "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
 
   metric :: "state => nat"
     "metric s == card {v. ~ s v}"
@@ -60,7 +60,7 @@
 
 declare reach_invariant_def [THEN def_set_simp, simp]
 
-lemma reach_invariant: "Rprg : Always reach_invariant"
+lemma reach_invariant: "Rprg \<in> Always reach_invariant"
 apply (rule AlwaysI, force) 
 apply (unfold Rprg_def, constrains) 
 apply (blast intro: rtrancl_trans)
@@ -71,7 +71,7 @@
 
 (*If it reaches a fixedpoint, it has found a solution*)
 lemma fixedpoint_invariant_correct: 
-     "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"
+     "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges^* }"
 apply (unfold fixedpoint_def)
 apply (rule equalityI)
 apply (auto intro!: ext)
@@ -80,7 +80,7 @@
 done
 
 lemma lemma1: 
-     "FP Rprg <= fixedpoint"
+     "FP Rprg \<subseteq> fixedpoint"
 apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto)
 apply (drule bspec, assumption)
 apply (simp add: Image_singleton image_iff)
@@ -88,7 +88,7 @@
 done
 
 lemma lemma2: 
-     "fixedpoint <= FP Rprg"
+     "fixedpoint \<subseteq> FP Rprg"
 apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def)
 apply (auto intro!: ext)
 done
@@ -103,16 +103,15 @@
   a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
   *)
 
-lemma Compl_fixedpoint: "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})"
-apply (simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def, auto)
+lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
+apply (auto simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def)
  apply (rule fun_upd_idem, force)
 apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
 done
 
 lemma Diff_fixedpoint:
-     "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})"
-apply (simp add: Diff_eq Compl_fixedpoint, blast)
-done
+     "A - fixedpoint = (\<Union>(u,v)\<in>edges. A \<inter> {s. s u & ~ s v})"
+by (simp add: Diff_eq Compl_fixedpoint, blast)
 
 
 (*** Progress ***)
@@ -127,13 +126,13 @@
 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"
 by (erule Suc_metric [THEN subst], blast)
 
-lemma metric_le: "metric (s(y:=s x | s y)) <= metric s"
+lemma metric_le: "metric (s(y:=s x | s y)) \<le> metric s"
 apply (case_tac "s x --> s y")
 apply (auto intro: less_imp_le simp add: fun_upd_idem)
 done
 
 lemma LeadsTo_Diff_fixedpoint:
-     "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
+     "Rprg \<in> ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"
 apply (simp (no_asm) add: Diff_fixedpoint Rprg_def)
 apply (rule LeadsTo_UN, auto)
 apply (ensures_tac "asgt a b")
@@ -144,19 +143,19 @@
 done
 
 lemma LeadsTo_Un_fixedpoint:
-     "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)"
+     "Rprg \<in> (metric-`{m}) LeadsTo (metric-`(lessThan m) \<union> fixedpoint)"
 apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R]
                              subset_imp_LeadsTo], auto)
 done
 
 
 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
-lemma LeadsTo_fixedpoint: "Rprg : UNIV LeadsTo fixedpoint"
+lemma LeadsTo_fixedpoint: "Rprg \<in> UNIV LeadsTo fixedpoint"
 apply (rule LessThan_induct, auto)
 apply (rule LeadsTo_Un_fixedpoint)
 done
 
-lemma LeadsTo_correct: "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }"
+lemma LeadsTo_correct: "Rprg \<in> UNIV LeadsTo { %v. (init, v) \<in> edges^* }"
 apply (subst fixedpoint_invariant_correct [symmetric])
 apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
 done
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -23,8 +23,8 @@
 
 inductive "REACHABLE"
   intros
-   base: "v : V ==> ((v,v) : REACHABLE)"
-   step: "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
+   base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
+   step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
 
 constdefs
   reachable :: "vertex => state set"
@@ -37,65 +37,64 @@
   "nmsg_gt k  == %e. {s. k < nmsg s e}"
 
   nmsg_gte :: "nat => edge => state set"
-  "nmsg_gte k == %e. {s. k <= nmsg s e}"
+  "nmsg_gte k == %e. {s. k \<le> nmsg s e}"
 
   nmsg_lte  :: "nat => edge => state set"
-  "nmsg_lte k  == %e. {s. nmsg s e <= k}"
-
-  
+  "nmsg_lte k  == %e. {s. nmsg s e \<le> k}"
 
   final :: "state set"
-  "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
+  "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> 
+            (INTER E (nmsg_eq 0))"
 
 axioms
 
-    Graph1: "root : V"
+    Graph1: "root \<in> V"
 
-    Graph2: "(v,w) : E ==> (v : V) & (w : V)"
+    Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)"
 
-    MA1:  "F : Always (reachable root)"
+    MA1:  "F \<in> Always (reachable root)"
 
-    MA2:  "v: V ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
+    MA2:  "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})"
 
-    MA3:  "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
+    MA3:  "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))"
 
-    MA4:  "(v,w) : E ==> 
-           F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
+    MA4:  "(v,w) \<in> E ==> 
+           F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))"
 
-    MA5:  "[|v:V; w:V|] 
-           ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
+    MA5:  "[|v \<in> V; w \<in> V|] 
+           ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))"
 
-    MA6:  "[|v:V|] ==> F : Stable (reachable v)"
+    MA6:  "[|v \<in> V|] ==> F \<in> Stable (reachable v)"
 
-    MA6b: "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
+    MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))"
 
-    MA7:  "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
+    MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
 
 
 lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
 lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
 
 lemma lemma2:
-     "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v"
+     "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
 apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L])
 apply (rule_tac [3] MA6)
 apply (auto simp add: E_imp_in_V_L E_imp_in_V_R)
 done
 
-lemma Induction_base: "(v,w) : E ==> F : reachable v LeadsTo reachable w"
+lemma Induction_base: "(v,w) \<in> E ==> F \<in> reachable v LeadsTo reachable w"
 apply (rule MA4 [THEN Always_LeadsTo_weaken])
 apply (rule_tac [2] lemma2)
 apply (auto simp add: nmsg_eq_def nmsg_gt_def)
 done
 
 lemma REACHABLE_LeadsTo_reachable:
-     "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w"
+     "(v,w) \<in> REACHABLE ==> F \<in> reachable v LeadsTo reachable w"
 apply (erule REACHABLE.induct)
 apply (rule subset_imp_LeadsTo, blast)
 apply (blast intro: LeadsTo_Trans Induction_base)
 done
 
-lemma Detects_part1: "F : {s. (root,v) : REACHABLE} LeadsTo reachable v"
+lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
 apply (rule single_LeadsTo_I)
 apply (simp split add: split_if_asm)
 apply (rule MA1 [THEN Always_LeadsToI])
@@ -104,7 +103,7 @@
 
 
 lemma Reachability_Detected: 
-     "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}"
+     "v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}"
 apply (unfold Detects_def, auto)
  prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
 apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
@@ -112,7 +111,7 @@
 
 
 lemma LeadsTo_Reachability:
-     "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})"
+     "v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})"
 by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
 
 
@@ -121,17 +120,15 @@
 (* Some lemmas about <==> *)
 
 lemma Eq_lemma1: 
-     "(reachable v <==> {s. (root,v) : REACHABLE}) =  
-      {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
-apply (unfold Equality_def, blast)
-done
+     "(reachable v <==> {s. (root,v) \<in> REACHABLE}) =  
+      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, blast)
 
 
 lemma Eq_lemma2: 
-     "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) =  
-      {s. ((s : reachable v) = ((root,v) : REACHABLE))}"
-apply (unfold Equality_def, auto)
-done
+     "(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) =  
+      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, auto)
 
 (* ------------------------------------ *)
 
@@ -139,37 +136,37 @@
 (* Some lemmas about final (I don't need all of them!)  *)
 
 lemma final_lemma1: 
-     "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) &  
-                              s : nmsg_eq 0 (v,w)})  
-      <= final"
+     "(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) &  
+                              s \<in> nmsg_eq 0 (v,w)})  
+      \<subseteq> final"
 apply (unfold final_def Equality_def, auto)
 apply (frule E_imp_in_V_R)
 apply (frule E_imp_in_V_L, blast)
 done
 
 lemma final_lemma2: 
- "E~={}  
-  ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))}  
-                           Int nmsg_eq 0 e)    <=  final"
+ "E\<noteq>{}  
+  ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}  
+                           \<inter> nmsg_eq 0 e)    \<subseteq>  final"
 apply (unfold final_def Equality_def)
 apply (auto split add: split_if_asm)
 apply (frule E_imp_in_V_L, blast)
 done
 
 lemma final_lemma3:
-     "E~={}  
-      ==> (INT v: V. INT e: E.  
-           (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)  
-          <= final"
+     "E\<noteq>{}  
+      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
+           (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
+          \<subseteq> final"
 apply (frule final_lemma2)
 apply (simp (no_asm_use) add: Eq_lemma2)
 done
 
 
 lemma final_lemma4:
-     "E~={}  
-      ==> (INT v: V. INT e: E.  
-           {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e)  
+     "E\<noteq>{}  
+      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
+           {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e)  
           = final"
 apply (rule subset_antisym)
 apply (erule final_lemma2)
@@ -177,9 +174,9 @@
 done
 
 lemma final_lemma5:
-     "E~={}  
-      ==> (INT v: V. INT e: E.  
-           ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)  
+     "E\<noteq>{}  
+      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
+           ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
           = final"
 apply (frule final_lemma4)
 apply (simp (no_asm_use) add: Eq_lemma2)
@@ -187,9 +184,9 @@
 
 
 lemma final_lemma6:
-     "(INT v: V. INT w: V.  
-       (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w))  
-      <= final"
+     "(\<Inter>v \<in> V. \<Inter>w \<in> V.  
+       (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))  
+      \<subseteq> final"
 apply (simp (no_asm) add: Eq_lemma2 Int_def)
 apply (rule final_lemma1)
 done
@@ -197,9 +194,9 @@
 
 lemma final_lemma7: 
      "final =  
-      (INT v: V. INT w: V.  
-       ((reachable v) <==> {s. (root,v) : REACHABLE}) Int  
-       (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))"
+      (\<Inter>v \<in> V. \<Inter>w \<in> V.  
+       ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
+       (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
 apply (unfold final_def)
 apply (rule subset_antisym, blast)
 apply (auto split add: split_if_asm)
@@ -213,56 +210,55 @@
 
 (* Stability theorems *)
 lemma not_REACHABLE_imp_Stable_not_reachable:
-     "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)"
+     "[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> Stable (- reachable v)"
 apply (drule MA2 [THEN AlwaysD], auto)
 done
 
 lemma Stable_reachable_EQ_R:
-     "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})"
+     "v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> REACHABLE})"
 apply (simp (no_asm) add: Equality_def Eq_lemma2)
 apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable)
 done
 
 
 lemma lemma4: 
-     "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int 
-       (- nmsg_gt 0 (v,w) Un A))  
-      <= A Un nmsg_eq 0 (v,w)"
+     "((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
+       (- nmsg_gt 0 (v,w) \<union> A))  
+      \<subseteq> A \<union> nmsg_eq 0 (v,w)"
 apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
 done
 
 
 lemma lemma5: 
-     "reachable v Int nmsg_eq 0 (v,w) =  
-      ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int  
-       (reachable v Int nmsg_lte 0 (v,w)))"
-apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
-done
+     "reachable v \<inter> nmsg_eq 0 (v,w) =  
+      ((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
+       (reachable v \<inter> nmsg_lte 0 (v,w)))"
+by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
 
 lemma lemma6: 
-     "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v"
+     "- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v"
 apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
 done
 
 lemma Always_reachable_OR_nmsg_0:
-     "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))"
+     "[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> nmsg_eq 0 (v,w))"
 apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken])
 apply (rule_tac [5] lemma4, auto)
 done
 
 lemma Stable_reachable_AND_nmsg_0:
-     "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))"
+     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> nmsg_eq 0 (v,w))"
 apply (subst lemma5)
 apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b)
 done
 
 lemma Stable_nmsg_0_OR_reachable:
-     "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)"
+     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)"
 by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
 
 lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0:
-     "[| v : V; w:V; (root,v) ~: REACHABLE |]  
-      ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))"
+     "[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |]  
+      ==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))"
 apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] 
                            Stable_nmsg_0_OR_reachable, 
             THEN Stable_eq])
@@ -271,8 +267,8 @@
 done
 
 lemma Stable_reachable_EQ_R_AND_nmsg_0:
-     "[| v : V; w:V |]  
-      ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int  
+     "[| v \<in> V; w \<in> V |]  
+      ==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
                       nmsg_eq 0 (v,w))"
 by (simp add: Equality_def Eq_lemma2  Stable_reachable_AND_nmsg_0
               not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0)
@@ -284,13 +280,13 @@
 
 (* LeadsTo final predicate (Exercise 11.2 page 274) *)
 
-lemma UNIV_lemma: "UNIV <= (INT v: V. UNIV)"
+lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)"
 by blast
 
 lemmas UNIV_LeadsTo_completion = 
     LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
 
-lemma LeadsTo_final_E_empty: "E={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final"
 apply (unfold final_def, simp)
 apply (rule UNIV_LeadsTo_completion)
   apply safe
@@ -300,13 +296,13 @@
 
 
 lemma Leadsto_reachability_AND_nmsg_0:
-     "[| v : V; w:V |]  
-      ==> F : UNIV LeadsTo  
-             ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))"
+     "[| v \<in> V; w \<in> V |]  
+      ==> F \<in> UNIV LeadsTo  
+             ((reachable v <==> {s. (root,v): REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
 apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
 apply (subgoal_tac
-	 "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int 
-              UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int 
+	 "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
+              UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
               nmsg_eq 0 (v,w) ")
 apply simp
 apply (rule PSP_Stable2)
@@ -314,7 +310,7 @@
 apply (rule_tac [3] Stable_reachable_EQ_R, auto)
 done
 
-lemma LeadsTo_final_E_NOT_empty: "E~={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> UNIV LeadsTo final"
 apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma])
 apply (rule_tac [2] final_lemma6)
 apply (rule Finite_stable_completion)
@@ -324,9 +320,9 @@
                     Leadsto_reachability_AND_nmsg_0)+
 done
 
-lemma LeadsTo_final: "F : UNIV LeadsTo final"
+lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
 apply (case_tac "E={}")
-apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
+ apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
 apply (rule LeadsTo_final_E_empty, auto)
 done
 
@@ -334,21 +330,23 @@
 
 (* Stability of final (Exercise 11.2 page 274) *)
 
-lemma Stable_final_E_empty: "E={} ==> F : Stable final"
+lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final"
 apply (unfold final_def, simp)
 apply (rule Stable_INT)
 apply (drule Stable_reachable_EQ_R, simp)
 done
 
 
-lemma Stable_final_E_NOT_empty: "E~={} ==> F : Stable final"
+lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> Stable final"
 apply (subst final_lemma7)
 apply (rule Stable_INT)
 apply (rule Stable_INT)
 apply (simp (no_asm) add: Eq_lemma2)
 apply safe
 apply (rule Stable_eq)
-apply (subgoal_tac [2] "({s. (s : reachable v) = ((root,v) : REACHABLE) } Int nmsg_eq 0 (v,w)) = ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int (- UNIV Un nmsg_eq 0 (v,w))) ")
+apply (subgoal_tac [2]
+     "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) = 
+      ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
 prefer 2 apply blast 
 prefer 2 apply blast 
 apply (rule Stable_reachable_EQ_R_AND_nmsg_0
@@ -358,15 +356,15 @@
  apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const])
  apply simp
 apply (subgoal_tac 
-        "({s. (s : reachable v) = ((root,v) : REACHABLE) }) = 
-         ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int
-              (- {} Un nmsg_eq 0 (v,w)))")
+        "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) = 
+         ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } Int
+              (- {} \<union> nmsg_eq 0 (v,w)))")
 apply blast+
 done
 
-lemma Stable_final: "F : Stable final"
+lemma Stable_final: "F \<in> Stable final"
 apply (case_tac "E={}")
-prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
+ prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
 apply (blast intro: Stable_final_E_empty)
 done
 
diff -r 3786b2fd6808 -r fd40c9d9076b src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy	Wed Feb 05 13:35:32 2003 +0100
@@ -41,23 +41,23 @@
       and next_def:
        "next i == (Suc i) mod N"
   assumes N_positive [iff]: "0<N"
-      and TR2:  "F : (T i) co (T i Un H i)"
-      and TR3:  "F : (H i) co (H i Un E i)"
-      and TR4:  "F : (H i - HasTok i) co (H i)"
-      and TR5:  "F : (HasTok i) co (HasTok i Un -(E i))"
-      and TR6:  "F : (H i Int HasTok i) leadsTo (E i)"
-      and TR7:  "F : (HasTok i) leadsTo (HasTok (next i))"
+      and TR2:  "F \<in> (T i) co (T i \<union> H i)"
+      and TR3:  "F \<in> (H i) co (H i \<union> E i)"
+      and TR4:  "F \<in> (H i - HasTok i) co (H i)"
+      and TR5:  "F \<in> (HasTok i) co (HasTok i \<union> -(E i))"
+      and TR6:  "F \<in> (H i \<inter> HasTok i) leadsTo (E i)"
+      and TR7:  "F \<in> (HasTok i) leadsTo (HasTok (next i))"
 
 
-lemma HasToK_partition: "[| s: HasTok i; s: HasTok j |] ==> i=j"
+lemma HasToK_partition: "[| s \<in> HasTok i; s \<in> HasTok j |] ==> i=j"
 by (unfold HasTok_def, auto)
 
-lemma not_E_eq: "(s ~: E i) = (s : H i | s : T i)"
+lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
 apply (simp add: H_def E_def T_def)
 apply (case_tac "proc s i", auto)
 done
 
-lemma (in Token) token_stable: "F : stable (-(E i) Un (HasTok i))"
+lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
 apply (unfold stable_def)
 apply (rule constrains_weaken)
 apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
@@ -74,7 +74,7 @@
 done
 
 lemma (in Token) nodeOrder_eq: 
-     "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"
+     "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> j)"
 apply (unfold nodeOrder_def next_def inv_image_def)
 apply (auto simp add: mod_Suc mod_geq)
 apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
@@ -84,7 +84,7 @@
   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
 lemma (in Token) TR7_nodeOrder:
      "[| i<N; j<N |] ==>    
-      F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"
+      F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
 apply (case_tac "i=j")
 apply (blast intro: subset_imp_leadsTo)
 apply (rule TR7 [THEN leadsTo_weaken_R])
@@ -93,19 +93,19 @@
 
 
 (*Chapter 4 variant, the one actually used below.*)
-lemma (in Token) TR7_aux: "[| i<N; j<N; i~=j |]     
-      ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"
+lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
+      ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
 apply (rule TR7 [THEN leadsTo_weaken_R])
 apply (auto simp add: HasTok_def nodeOrder_eq)
 done
 
 lemma (in Token) token_lemma:
-     "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})"
+     "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
 by auto
 
 
 (*Misra's TR9: the token reaches an arbitrary node*)
-lemma  (in Token) leadsTo_j: "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"
+lemma  (in Token) leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac I = "-{j}" and f = token and B = "{}" 
        in wf_nodeOrder [THEN bounded_induct])
@@ -118,7 +118,7 @@
 
 (*Misra's TR8: a hungry process eventually eats*)
 lemma (in Token) token_progress:
-     "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"
+     "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
 apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
 apply (rule_tac [2] TR6)
 apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+)