src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy

 apply (rule compatibility_consequence3)
 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1)
 done
 
 
-(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
+(* the next two theorems are only necessary, as there is no theorem ext (A\<parallel>B) = ext (B\<parallel>A) *)
 
 lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"
 apply auto
 done
 

              is_asig_of A1; is_asig_of A2;  
              is_asig_of B1; is_asig_of B2;  
              compatible A1 B1; compatible A2 B2;  
              A1 =<| A2;  
              B1 =<| B2 |]  
-         ==> (A1 || B1) =<| (A2 || B2)"
+         ==> (A1 \<parallel> B1) =<| (A2 \<parallel> B2)"
 apply (simp add: is_asig_of_def)
 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
 apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par)
 apply auto