--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:35:21 2015 +0100
@@ -23,7 +23,7 @@
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
@@ -46,7 +46,7 @@
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])