# HG changeset patch
# User wenzelm
# Date 1729593938 -7200
# Node ID e18600daa9042b0412ae97a3b7144e693ca9a47f
# Parent  ed326e93b835aeabc8c850dc0db52be7b1de723e
tuned comments;

diff -r ed326e93b835 -r e18600daa904 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:41:20 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:45:38 2024 +0200
@@ -1,5 +1,6 @@
 (*  Title:      Pure/Syntax/mixfix.ML
-    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
+    Author:     Tobias Nipkow, TU Muenchen
+    Author:     Makarius
 
 Mixfix declarations, infixes, binders.
 *)