NEWS
changeset 67419 866b1ad870ac
parent 67413 2555713586c8
child 67424 0b691782d6e5
     1.1 --- a/NEWS	Sat Jan 13 15:18:51 2018 +0100
     1.2 +++ b/NEWS	Sat Jan 13 15:49:59 2018 +0100
     1.3 @@ -118,10 +118,9 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* Unused formal text within inner syntax may be marked as
     1.8 -\<^cancel>\<open>text\<close>. Thus it is ignored within the formal language, but
     1.9 -still printed in the document (with special markup). This is an official
    1.10 -way to "comment-out" some text.
    1.11 +* \<^cancel>\<open>text\<close> marks unused text within inner syntax: it is ignored
    1.12 +within the formal language, but shown in the document with strike-out
    1.13 +style.
    1.14  
    1.15  * Embedded languages such as inner syntax and ML may contain formal
    1.16  comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer