diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Word.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -1684,13 +1684,13 @@
   by (simp flip: signed_take_bit_decr_length_iff)
 
 notation
-  word_sle    ("'(\<le>s')") and
-  word_sle    ("(_/ \<le>s _)"  [51, 51] 50) and
-  word_sless  ("'(<s')") and
-  word_sless  ("(_/ <s _)"  [51, 51] 50)
+  word_sle    (\<open>'(\<le>s')\<close>) and
+  word_sle    (\<open>(_/ \<le>s _)\<close>  [51, 51] 50) and
+  word_sless  (\<open>'(<s')\<close>) and
+  word_sless  (\<open>(_/ <s _)\<close>  [51, 51] 50)
 
 notation (input)
-  word_sle    ("(_/ <=s _)"  [51, 51] 50)
+  word_sle    (\<open>(_/ <=s _)\<close>  [51, 51] 50)
 
 lemma word_sle_eq [code]:
   \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>