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/Fixrec.thy
changeset 80914 d97fdabd9e2b
parent 69913 ca515cf61651
child 81574 c4abe6582ee5 
--- a/src/HOL/HOLCF/Fixrec.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -73,7 +73,7 @@
   "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))"
 
 abbreviation
-  mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr "+++" 65)  where
+  mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match"  (infixr \<open>+++\<close> 65)  where
   "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2"
 
 text \<open>rewrite rules for mplus\<close>
isabelle