diff -r 95f1e700b712 -r 57bf0cecb366 src/ZF/UNITY/Merge.thy
--- a/src/ZF/UNITY/Merge.thy	Tue Mar 06 16:46:27 2012 +0000
+++ b/src/ZF/UNITY/Merge.thy	Tue Mar 06 17:01:37 2012 +0000
@@ -107,14 +107,14 @@
 done
 
 lemma (in merge) merge_Allowed: 
-     "Allowed(M) = (preserves(lift(Out)) Int preserves(lift(iOut)))"
+     "Allowed(M) = (preserves(lift(Out)) \<inter> preserves(lift(iOut)))"
 apply (insert merge_spec preserves_type [of "lift (Out)"])
 apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def safety_prop_Acts_iff)
 done
 
 lemma (in merge) M_ok_iff: 
      "G \<in> program ==>  
-       M ok G <-> (G \<in> preserves(lift(Out)) &   
+       M ok G \<longleftrightarrow> (G \<in> preserves(lift(Out)) &   
                    G \<in> preserves(lift(iOut)) & M \<in> Allowed(G))"
 apply (cut_tac merge_spec)
 apply (auto simp add: merge_Allowed ok_iff_Allowed)
@@ -166,7 +166,7 @@
 apply (subgoal_tac "xa \<in> nat")
 apply (simp_all add: Ord_mem_iff_lt)
 prefer 2 apply (blast intro: lt_trans)
-apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) --> elt<Nclients" in bspec)
+apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
 apply (simp add: ltI nat_into_Ord)
 apply (blast dest: ltD)
 done