src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/Rat.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -1155,7 +1155,7 @@
 
 subsection \<open>Float syntax\<close>
 
-syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>_\<close>)
+syntax "_Float" :: "float_const \<Rightarrow> 'a"    (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>_)\<close>)
 
 parse_translation \<open>
   let