diff -r cc2d676d5395 -r 7d59af98af29 NEWS
--- a/NEWS	Wed Dec 26 16:25:20 2018 +0100
+++ b/NEWS	Wed Dec 26 20:57:23 2018 +0100
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* Old-style {* verbatim *} tokens are explicitly marked as legacy
+feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
+via "isabelle update_cartouches -t" (available since Isabelle2015).
+
 * The font family "Isabelle DejaVu" is systematically derived from the
 existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
 and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".