# HG changeset patch
# User wenzelm
# Date 1725224351 -7200
# Node ID 12efa7f92f35a53f80c4875317d30a713886ab9d
# Parent  5e38e8b34eb35e590e3e9ad4373d3742e496cabd
more NEWS;

diff -r 5e38e8b34eb3 -r 12efa7f92f35 NEWS
--- a/NEWS	Sun Sep 01 19:35:30 2024 +0200
+++ b/NEWS	Sun Sep 01 22:59:11 2024 +0200
@@ -28,6 +28,14 @@
 
 ** 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.