--- a/NEWS Wed Oct 02 18:32:36 2024 +0200
+++ b/NEWS Thu Oct 03 13:01:31 2024 +0200
@@ -9,6 +9,10 @@
*** General ***
+* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
+so its declarations are applied immediately, but also named for later
+re-use.
+
* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
@@ -43,6 +47,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.