# HG changeset patch
# User wenzelm
# Date 1728386033 -7200
# Node ID ef362328b93167fea4a2e8424d91f64380fbf936
# Parent  ec121999a9cbe3265571352d916f358f86023416
clarified mixfix annotations;

diff -r ec121999a9cb -r ef362328b931 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Tue Oct 08 12:10:35 2024 +0200
+++ b/src/ZF/Bin.thy	Tue Oct 08 13:13:53 2024 +0200
@@ -101,11 +101,11 @@
                                  NCons(bin_mult(v,w),0))"
 
 syntax
-  "_Int0" :: i  (\<open>#' 0\<close>)
-  "_Int1" :: i  (\<open>#' 1\<close>)
-  "_Int2" :: i  (\<open>#' 2\<close>)
-  "_Neg_Int1" :: i  (\<open>#-' 1\<close>)
-  "_Neg_Int2" :: i  (\<open>#-' 2\<close>)
+  "_Int0" :: i  (\<open>#()0\<close>)
+  "_Int1" :: i  (\<open>#()1\<close>)
+  "_Int2" :: i  (\<open>#()2\<close>)
+  "_Neg_Int1" :: i  (\<open>#-()1\<close>)
+  "_Neg_Int2" :: i  (\<open>#-()2\<close>)
 translations
   "#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
   "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"