--- a/src/ZF/Bin.thy Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/Bin.thy Sun Aug 25 15:07:22 2024 +0200
@@ -117,10 +117,11 @@
"_Int" :: "num_token \<Rightarrow> i" (\<open>#_\<close> 1000)
"_Neg_Int" :: "num_token \<Rightarrow> i" (\<open>#-_\<close> 1000)
+syntax_consts
+ "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
+
ML_file \<open>Tools/numeral_syntax.ML\<close>
-syntax_consts
- "_Int0" "_Int1" "_Int2" "_Int" "_Neg_Int1" "_Neg_Int2" "_Neg_Int" \<rightleftharpoons> integ_of
declare bin.intros [simp,TC]