src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
changeset 61999 89291b5d0ede
parent 58880 0baae4311a9f
child 62002 f1599e98c4d0
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -15,7 +15,7 @@
 
 definition
   impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
-  "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
+  "impl_fin_ioa = (sender_ioa \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel>
                   rsch_fin_ioa)"
 
 definition