| 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