Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/ex/Concurrency_Monad.thy
changeset 80914 d97fdabd9e2b
parent 62175 8ffc4d0e652d 
--- a/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/ex/Concurrency_Monad.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -200,7 +200,7 @@
 lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
 by (fixrec_simp, cases r, simp_all)
 
-abbreviation apR (infixl "\<diamondop>" 70)
+abbreviation apR (infixl \<open>\<diamondop>\<close> 70)
   where "a \<diamondop> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
 
 text \<open>Proofs that \<open>zipR\<close> satisfies the applicative functor laws:\<close>
isabelle