--- a/src/Doc/System/Sessions.thy Tue Dec 05 15:55:14 2017 +0100
+++ b/src/Doc/System/Sessions.thy Tue Dec 05 16:03:58 2017 +0100
@@ -195,6 +195,10 @@
possible to use different document variant names (without tags) for
different document root entries, see also \secref{sec:tool-document}.
+ \<^item> @{system_option_def "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 \<^verbatim>\<open>ROOT\<close>).
+
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For