*** 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.
This refers to Isabelle/386a31d6d17a.
An example session is attached.
Makarius
Test_Tags.tar.gz
Description: application/gzip
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
