# HG changeset patch
# User wenzelm
# Date 1452342677 -3600
# Node ID 8d75ff14e3e963f9c88e3e0a3943a4e2790134bd
# Parent  d65f80949ff1ce5ca5830aff96baef4f9c105cff
tuned syntax;

diff -r d65f80949ff1 -r 8d75ff14e3e9 src/HOL/HOLCF/ex/Concurrency_Monad.thy
--- 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)