diff -r 4c8280aaf6ad -r ba226b87c69e NEWS
--- a/NEWS	Sun Jan 07 12:41:34 2018 +0100
+++ b/NEWS	Sun Jan 07 13:45:21 2018 +0100
@@ -10,7 +10,8 @@
 *** General ***
 
 * Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
-marginal comments in outer syntax.
+marginal comments in outer syntax: antiquotations are supported as usual
+(wrt. the overall command context).
 
 * The old 'def' command has been discontinued (legacy since
 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with