--- a/NEWS Mon Jan 08 22:36:02 2018 +0100
+++ b/NEWS Mon Jan 08 23:45:43 2018 +0100
@@ -108,6 +108,10 @@
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.
+
* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).