diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Statespace/StateSpaceSyntax.thy
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -11,9 +11,9 @@
 can choose if you want to use it or not.\<close>
 
 syntax 
-  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
+  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (\<open>_\<cdot>_\<close> [60, 60] 60)
   "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
-  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
+  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  (\<open>_<_>\<close> [900, 0] 900)
 
 translations
   "_statespace_updates f (_updbinds b bs)" ==