
diff -r c531629c391a -r 6ce0c8d59f5a src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Oct 06 21:55:31 2024 +0200
+++ b/src/HOL/Num.thy	Sun Oct 06 22:56:07 2024 +0200
@@ -302,7 +302,7 @@
 text \<open>Numeral syntax.\<close>
 
 syntax
-  "_Numeral" :: "num_const \<Rightarrow> 'a"    (\<open>_\<close>)
+  "_Numeral" :: "num_const \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>_)\<close>)
 
 ML_file \<open>Tools/numeral.ML\<close>
 




