src/HOL/UNITY/Comp/Alloc.thy

 
 axiomatization Network :: "'a systemState program"
   where Network: "Network : network_spec"
 
 definition System  :: "'a systemState program"
-  where "System = rename sysOfAlloc Alloc Join Network Join
+  where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion>
                  (rename sysOfClient
                   (plam x: lessThan Nclients. rename client_map Client))"
 
 
 (**

     Network "Network : network_spec"
 
   defines
     System_def
       "System == rename sysOfAlloc Alloc
-                 Join
+                 \<squnion>
                  Network
-                 Join
+                 \<squnion>
                  (rename sysOfClient
                   (plam x: lessThan Nclients. rename client_map Client))"
 **)
 
 declare subset_preserves_o [THEN [2] rev_subsetD, intro]

   Alloc_preserves_dummy [iff]
 
 
 subsection{*Components Lemmas [MUST BE AUTOMATED]*}
 
-lemma Network_component_System: "Network Join
+lemma Network_component_System: "Network \<squnion>
       ((rename sysOfClient
-        (plam x: (lessThan Nclients). rename client_map Client)) Join
+        (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
        rename sysOfAlloc Alloc)
       = System"
   by (simp add: System_def Join_ac)
 
 lemma Client_component_System: "(rename sysOfClient
-       (plam x: (lessThan Nclients). rename client_map Client)) Join
-      (Network Join rename sysOfAlloc Alloc)  =  System"
+       (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
+      (Network \<squnion> rename sysOfAlloc Alloc)  =  System"
   by (simp add: System_def Join_ac)
 
-lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
-       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
+lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion>
+       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
         Network)  =  System"
   by (simp add: System_def Join_ac)
 
 declare
   Client_component_System [iff]