# HG changeset patch
# User wenzelm
# Date 1727860125 -7200
# Node ID 21faacc45c0c98f0232911867cb7061270a8b4f5
# Parent  6c81cdca5b82585acebafea3dca531342e196c8b
more NEWS;

diff -r 6c81cdca5b82 -r 21faacc45c0c NEWS
--- a/NEWS	Wed Oct 02 10:35:44 2024 +0200
+++ b/NEWS	Wed Oct 02 11:08:45 2024 +0200
@@ -28,6 +28,19 @@
 
 *** HOL ***
 
+* Various declaration bundles support adhoc modification of notation,
+notably like this:
+
+  unbundle no_list_syntax
+  unbundle no_listcompr_syntax
+  unbundle no_rtrancl_syntax
+  unbundle no_trancl_syntax
+  unbundle no_reflcl_syntax
+
+This is more robust than individual 'no_syntax' / 'no_notation'
+commands, which need to copy mixfix declarations from elsewhere and thus
+break after changes in the library.
+
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITIES.