| changeset 81124 | 6ce0c8d59f5a |
| parent 80932 | 261cd8722677 |
| child 81980 | 13b5aa1b3fb4 |
--- 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>