--- a/NEWS Tue Dec 05 15:55:14 2017 +0100
+++ b/NEWS Tue Dec 05 16:03:58 2017 +0100
@@ -68,6 +68,17 @@
arguments into this format.
+*** Document preparation ***
+
+* 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).
+
+* Document markup commands ('section', 'text' etc.) are implicitly
+tagged as "document" and visible by default. This avoids the application
+of option "document_tags" to these commands.
+
+
*** HOL ***
* SMT module: