tuned;
authorwenzelm
Sat Jan 13 15:49:59 2018 +0100 (18 months ago)
changeset 67419866b1ad870ac
parent 67418 5a6ed2e679fb
child 67420 c4c8787ed669
tuned;
NEWS
     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