# 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 \'a list\} vs. @{ML_type 'a \list\}; @{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