--- a/src/HOL/HOLCF/Ssum.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Ssum.thy Fri Sep 20 19:51:08 2024 +0200
@@ -19,14 +19,14 @@
(fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
(fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
-pcpodef ('a, 'b) ssum ("(_ \<oplus>/ _)" [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
by (simp_all add: ssum_def)
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
type_notation (ASCII)
- ssum (infixr "++" 10)
+ ssum (infixr \<open>++\<close> 10)
subsection \<open>Definitions of constructors\<close>