# HG changeset patch
# User wenzelm
# Date 1728562398 -7200
# Node ID 87f173836d5667137b5fe2b1f4ff878449c93704
# Parent  c9f1e926d4ed54a13e3398f58a66200db7272bb3
tuned NEWS;

diff -r c9f1e926d4ed -r 87f173836d56 NEWS
--- a/NEWS	Thu Oct 10 12:20:24 2024 +0200
+++ b/NEWS	Thu Oct 10 14:13:18 2024 +0200
@@ -33,7 +33,11 @@
 "infix" and "binder" declarations are automatic, but general mixfix
 forms require manual annotations in the theory library. Plenty of
 existing examples may be found in the Isabelle sources by searching for
-"notation=" (without quotes and no extra space).
+"notation=" (without quotes and no extra space). Occasional
+INCOMPATIBILITY for 'no_syntax' or 'no_notation' declarations in user
+applications: the mixfix template needs to be adapted accordingly, but
+it is often better to use "unbundle no foobar_syntax", as explained for
+HOL libraries below.
 
 * Inner syntax translations now support formal dependencies via commands
 'syntax_types' or 'syntax_consts'. This is essentially an abstract