# HG changeset patch
# User wenzelm
# Date 1621793556 -7200
# Node ID d07ab5b144538696166d6ae493619b08d3ee31d1
# Parent  1419cb7f7f3eec5356871481112d1b41cc7eb1db
NEWS;

diff -r 1419cb7f7f3e -r d07ab5b14453 NEWS
--- a/NEWS	Sun May 23 19:59:37 2021 +0200
+++ b/NEWS	Sun May 23 20:12:36 2021 +0200
@@ -34,6 +34,13 @@
 
 *** Document preparation ***
 
+* Document antiquotations for ML text have been refined: "def" and "ref"
+variants support index entries, e.g. @{ML} (no entry) vs. @{ML_def}
+(bold entry) vs. @{ML_ref} (regular entry); @{ML_type} supports explicit
+type arguments for constructors (only relevant for index), e.g.
+@{ML_type \<open>'a list\<close>} vs. @{ML_type 'a \<open>list\<close>}; @{ML_op} has been renamed
+to @{ML_infix}. Minor INCOMPATIBILITY concerning name and syntax.
+
 * Option "document_logo" determines if an instance of the Isabelle logo
 should be created in the document output directory. The given string
 specifies the name of the logo variant, while "_" (underscore) refers to