diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -98,7 +98,7 @@
       simultaneously. *}
 lemma ask_bounded_lemma:
      "Client ok G   
-      ==> Client Join G \<in>   
+      ==> Client \<squnion> G \<in>   
               Always ({s. tok s \<le> NbT}  Int   
                       {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
 apply auto
@@ -125,13 +125,13 @@
 by (simp add: Client_def, safety, auto)
 
 lemma Join_Stable_rel_le_giv:
-     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
-      ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
+     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client \<squnion> G \<in> Stable {s. rel s \<le> giv s}"
 by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
 
 lemma Join_Always_rel_le_giv:
-     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
-      ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
+     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client \<squnion> G \<in> Always {s. rel s \<le> giv s}"
 by (force intro: AlwaysI Join_Stable_rel_le_giv)
 
 lemma transient_lemma:
@@ -146,8 +146,8 @@
 
 
 lemma induct_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-  ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+  ==> Client \<squnion> G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
                       LeadsTo {s. k < rel s & rel s \<le> giv s &  
                                   h \<le> giv s & h pfixGe ask s}"
 apply (rule single_LeadsTo_I)
@@ -165,8 +165,8 @@
 
 
 lemma rel_progress_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-  ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+  ==> Client \<squnion> G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
                       LeadsTo {s. h \<le> rel s}"
 apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
 apply (auto simp add: vimage_def)
@@ -179,8 +179,8 @@
 
 
 lemma client_progress_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-      ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+      ==> Client \<squnion> G \<in> {s. h \<le> giv s & h pfixGe ask s}   
                           LeadsTo {s. h \<le> rel s}"
 apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
 apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])