
diff -r 66893c47500d -r 701912f5645a src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/Bin.thy	Fri Aug 23 23:14:39 2024 +0200
@@ -119,6 +119,8 @@
 
 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]
 




