--- a/src/ZF/Bin.thy Sun Oct 06 21:55:31 2024 +0200
+++ b/src/ZF/Bin.thy Sun Oct 06 22:56:07 2024 +0200
@@ -114,8 +114,8 @@
"#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
syntax
- "_Int" :: "num_token \<Rightarrow> i" (\<open>#_\<close> 1000)
- "_Neg_Int" :: "num_token \<Rightarrow> i" (\<open>#-_\<close> 1000)
+ "_Int" :: "num_token \<Rightarrow> i" (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>#_)\<close> 1000)
+ "_Neg_Int" :: "num_token \<Rightarrow> i" (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>#-_)\<close> 1000)
syntax_consts
"_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of