# HG changeset patch
# User wenzelm
# Date 1728475976 -7200
# Node ID d74e53f674748fd7c88795fd0e180fcaa515f0de
# Parent  affe64a29f566d4cc87dfdc668c09de4134a8c9f
more NEWS;

diff -r affe64a29f56 -r d74e53f67474 NEWS
--- a/NEWS	Wed Oct 09 14:08:13 2024 +0200
+++ b/NEWS	Wed Oct 09 14:12:56 2024 +0200
@@ -81,6 +81,13 @@
 commands, which need to copy mixfix declarations from elsewhere and thus
 break after changes in the library.
 
+* Theory "HOL-Library.Datatype_Records" provides bundle
+"datatype_record_syntax" to exchange its alternative notation versus
+regular "record_syntax". This also allows to swap record syntax later
+on, notably like this:
+
+  unbundle no datatype_record_syntax
+
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITY.