src/HOL/SPARK/Manual/Reference.thy

--- a/src/HOL/SPARK/Manual/Reference.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,7 +9,7 @@
   by (simp flip: mask_eq_exp_minus_1 take_bit_eq_mask take_bit_eq_mod)
 
 syntax (my_constrain output)
-  "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+  "_constrain" :: "logic => type => logic" (\<open>_ :: _\<close> [4, 0] 3)
 (*>*)
 
 chapter \<open>HOL-\SPARK{} Reference\<close>