# HG changeset patch
# User wenzelm
# Date 1515854999 -3600
# Node ID 866b1ad870acc982361f91e1cd570c3c1969d9dc
# Parent  5a6ed2e679fbef82e36850ce9832eff3efe796a3
tuned;

diff -r 5a6ed2e679fb -r 866b1ad870ac NEWS
--- a/NEWS	Sat Jan 13 15:18:51 2018 +0100
+++ b/NEWS	Sat Jan 13 15:49:59 2018 +0100
@@ -118,10 +118,9 @@
 
 *** Document preparation ***
 
-* Unused formal text within inner syntax may be marked as
-\<^cancel>\<open>text\<close>. Thus it is ignored within the formal language, but
-still printed in the document (with special markup). This is an official
-way to "comment-out" some text.
+* \<^cancel>\<open>text\<close> marks unused text within inner syntax: it is ignored
+within the formal language, but shown in the document with strike-out
+style.
 
 * Embedded languages such as inner syntax and ML may contain formal
 comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer