--- 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>