NEWS
changeset 67424 0b691782d6e5
parent 67419 866b1ad870ac
child 67433 e0c0c1f0e3e7
     1.1 --- a/NEWS	Sat Jan 13 20:30:52 2018 +0100
     1.2 +++ b/NEWS	Sat Jan 13 21:41:36 2018 +0100
     1.3 @@ -118,9 +118,8 @@
     1.4  
     1.5  *** Document preparation ***
     1.6  
     1.7 -* \<^cancel>\<open>text\<close> marks unused text within inner syntax: it is ignored
     1.8 -within the formal language, but shown in the document with strike-out
     1.9 -style.
    1.10 +* \<^cancel>\<open>text\<close> cancels unused text within inner syntax: it is ignored within
    1.11 +the formal language, but shown in the document with strike-out style.
    1.12  
    1.13  * Embedded languages such as inner syntax and ML may contain formal
    1.14  comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer