NEWS
changeset 67140 386a31d6d17a
parent 67133 540eeaf88a63
child 67145 e77c5bfca9aa
     1.1 --- a/NEWS	Tue Dec 05 15:55:14 2017 +0100
     1.2 +++ b/NEWS	Tue Dec 05 16:03:58 2017 +0100
     1.3 @@ -68,6 +68,17 @@
     1.4  arguments into this format.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* System option "document_tags" specifies a default for otherwise
    1.10 +untagged commands. This is occasionally useful to control the global
    1.11 +visibility of commands via session options (e.g. in ROOT).
    1.12 +
    1.13 +* Document markup commands ('section', 'text' etc.) are implicitly
    1.14 +tagged as "document" and visible by default. This avoids the application
    1.15 +of option "document_tags" to these commands.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * SMT module: