src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Rat.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -800,7 +800,7 @@
 context field_char_0
 begin
 
-definition Rats :: "'a set" ("\<rat>")
+definition Rats :: "'a set" (\<open>\<rat>\<close>)
   where "\<rat> = range of_rat"
 
 end
@@ -1155,7 +1155,7 @@
 
 subsection \<open>Float syntax\<close>
 
-syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>_\<close>)
 
 parse_translation \<open>
   let