NEWS
changeset 67510 9624711ef2de
parent 67507 5db077cfe1b2
child 67525 5d04d7bcd5f6
     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.