Sun, 23 May 2021 20:12:36 +0200
changeset 73771 d07ab5b14453
parent 73770 1419cb7f7f3e
child 73772 6b4c47666267
--- 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