--- a/src/HOL/HOLCF/ex/Concurrency_Monad.thy Sat Jan 09 13:00:04 2016 +0100
+++ b/src/HOL/HOLCF/ex/Concurrency_Monad.thy Sat Jan 09 13:31:17 2016 +0100
@@ -200,23 +200,23 @@
lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
by (fixrec_simp, cases r, simp_all)
-abbreviation apR (infixl "\<diamond>" 70)
- where "a \<diamond> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
+abbreviation apR (infixl "\<diamondop>" 70)
+ where "a \<diamondop> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
-lemma R_homomorphism: "Done\<cdot>f \<diamond> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
+lemma R_homomorphism: "Done\<cdot>f \<diamondop> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
by simp
-lemma R_identity: "Done\<cdot>ID \<diamond> r = r"
+lemma R_identity: "Done\<cdot>ID \<diamondop> r = r"
by (induct r, simp_all add: mapN_mapN eta_cfun)
-lemma R_interchange: "r \<diamond> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamond> r"
+lemma R_interchange: "r \<diamondop> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamondop> r"
by (induct r, simp_all add: mapN_mapN)
text {* The associativity rule is the hard one! *}
-lemma R_associativity: "Done\<cdot>cfcomp \<diamond> r1 \<diamond> r2 \<diamond> r3 = r1 \<diamond> (r2 \<diamond> r3)"
+lemma R_associativity: "Done\<cdot>cfcomp \<diamondop> r1 \<diamondop> r2 \<diamondop> r3 = r1 \<diamondop> (r2 \<diamondop> r3)"
proof (induct r1 arbitrary: r2 r3)
case (Done x1) thus ?case
proof (induct r2 arbitrary: r3)