Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified mixfix annotations;
authorwenzelm
Tue, 08 Oct 2024 13:13:53 +0200
changeset 81126 ef362328b931
parent 81125 ec121999a9cb
child 81127 12990a6dddcb
clarified mixfix annotations;
src/ZF/Bin.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle