redundant;
authorwenzelm
Fri Jan 26 21:16:03 2018 +0100 (16 months ago)
changeset 675109624711ef2de
parent 67509 524dc5c2a031
child 67511 a6f5a78712af
redundant;
NEWS
     1.1 --- a/NEWS	Thu Jan 25 16:50:27 2018 +0100
     1.2 +++ b/NEWS	Fri Jan 26 21:16:03 2018 +0100
     1.3 @@ -136,11 +136,6 @@
     1.4    - canceled source: \<^cancel>\<open>\<dots>\<close>
     1.5    - raw LaTeX: \<^latex>\<open>\<dots>\<close>
     1.6  
     1.7 -* Embedded languages such as inner syntax and ML may contain formal
     1.8 -comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
     1.9 -syntax, antiquotations are interpreted wrt. the presentation context of
    1.10 -the enclosing command.
    1.11 -
    1.12  * Outside of the inner theory body, the default presentation context is
    1.13  theory Pure. Thus elementary antiquotations may be used in markup
    1.14  commands (e.g. 'chapter', 'section', 'text') and formal comments.