# HG changeset patch
# User wenzelm
# Date 1516997763 -3600
# Node ID 9624711ef2de43fc0837a4900c3b08b9f47120c6
# Parent  524dc5c2a03173c6d33096984b82ef16ef23b87f
redundant;

diff -r 524dc5c2a031 -r 9624711ef2de NEWS
--- a/NEWS	Thu Jan 25 16:50:27 2018 +0100
+++ b/NEWS	Fri Jan 26 21:16:03 2018 +0100
@@ -136,11 +136,6 @@
   - canceled source: \<^cancel>\<open>\<dots>\<close>
   - raw LaTeX: \<^latex>\<open>\<dots>\<close>
 
-* Embedded languages such as inner syntax and ML may contain formal
-comments of the form "\<comment> \<open>text\<close>". As in marginal comments of outer
-syntax, antiquotations are interpreted wrt. the presentation context of
-the enclosing command.
-
 * Outside of the inner theory body, the default presentation context is
 theory Pure. Thus elementary antiquotations may be used in markup
 commands (e.g. 'chapter', 'section', 'text') and formal comments.