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