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 \Numeral syntax.\ syntax - "_Numeral" :: "num_const \ 'a" (\_\) + "_Numeral" :: "num_const \ 'a" (\(\open_block notation=\literal number\\_)\) ML_file \Tools/numeral.ML\