--- a/NEWS Mon Sep 30 13:00:42 2024 +0200
+++ b/NEWS Mon Sep 30 20:30:59 2024 +0200
@@ -28,14 +28,6 @@
*** HOL ***
-* Enumerations for tuples, sets, lists etc. now use specific grammar
-productions and separate syntax constants: this allows PIDE markup
-(hyperlinks) for the separators (commas). For example, instead of
-generic nonterminal "args" and syntax constant "_args" from Pure, HOL
-lists now use nonterminal "list_args" and syntax constant "_list_args".
-Rare INCOMPATIBILITY for ambitious syntax translations and grammar
-modifications (e.g. via 'no_syntax').
-
* Theory "HOL.Wellfounded":
- Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
Minor INCOMPATIBILITIES.