diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Hoare/Separation.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -19,7 +19,7 @@
 
 text\<open>The semantic definition of a few connectives:\<close>
 
-definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
+definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix \<open>\<bottom>\<close> 55)
   where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
 
 definition is_empty :: "heap \<Rightarrow> bool"
@@ -51,10 +51,10 @@
 bound Hs - otherwise they may bind the implicit H.\<close>
 
 syntax
- "_emp" :: "bool" ("emp")
- "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" ("[_ \<mapsto> _]")
- "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
- "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
+ "_emp" :: "bool" (\<open>emp\<close>)
+ "_singl" :: "nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>[_ \<mapsto> _]\<close>)
+ "_star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>**\<close> 60)
+ "_wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl \<open>-*\<close> 60)
 
 (* FIXME does not handle "_idtdummy" *)
 ML \<open>