diff -r 95f1e700b712 -r 57bf0cecb366 src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Tue Mar 06 16:46:27 2012 +0000
+++ b/src/ZF/UNITY/ClientImpl.thy	Tue Mar 06 17:01:37 2012 +0000
@@ -91,7 +91,7 @@
 declare  client_ask_act_def [THEN def_act_simp, simp]
 
 lemma client_prog_ok_iff:
-  "\<forall>G \<in> program. (client_prog ok G) <->  
+  "\<forall>G \<in> program. (client_prog ok G) \<longleftrightarrow>  
    (G \<in> preserves(lift(rel)) & G \<in> preserves(lift(ask)) &  
     G \<in> preserves(lift(tok)) &  client_prog \<in> Allowed(G))"
 by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed])
@@ -117,7 +117,7 @@
 
 (*Safety property 1: ask, rel are increasing: (24) *)
 lemma client_prog_Increasing_ask_rel: 
-"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"
+"client_prog: program guarantees Incr(lift(ask)) \<inter> Incr(lift(rel))"
 apply (unfold guar_def)
 apply (auto intro!: increasing_imp_Increasing 
             simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
@@ -137,7 +137,7 @@
 lemma ask_Bounded_lemma: 
 "[| client_prog ok G; G \<in> program |] 
       ==> client_prog \<squnion> G \<in>    
-              Always({s \<in> state. s`tok \<le> NbT}  Int   
+              Always({s \<in> state. s`tok \<le> NbT}  \<inter>   
                       {s \<in> state. \<forall>elt \<in> set_of_list(s`ask). elt \<le> NbT})"
 apply (rotate_tac -1)
 apply (auto simp add: client_prog_ok_iff)
@@ -209,7 +209,7 @@
 done
 
 lemma strict_prefix_is_prefix: 
-    "<xs, ys> \<in> strict_prefix(A) <->  <xs, ys> \<in> prefix(A) & xs\<noteq>ys"
+    "<xs, ys> \<in> strict_prefix(A) \<longleftrightarrow>  <xs, ys> \<in> prefix(A) & xs\<noteq>ys"
 apply (unfold strict_prefix_def id_def lam_def)
 apply (auto dest: prefix_type [THEN subsetD])
 done
@@ -298,7 +298,7 @@
 
 lemma client_prog_Allowed:
      "Allowed(client_prog) =  
-      preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))"
+      preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
 apply (cut_tac v = "lift (ask)" in preserves_type)
 apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed] 
                       cons_Int_distrib safety_prop_Acts_iff)