[isabelle-dev] NEWS: document_tags

Tobias Nipkow nipkow at in.tum.de
Wed Dec 6 09:56:53 CET 2017

On 05/12/2017 17:21, Makarius wrote:
> *** 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.

Thanks for this. Just a bit of context info: this simplifies the creation of 
documents where only a few key parts of a theory are shown (eg main definitions 
and thms). This in turn can be used to produce readable documentation for large 
sessions (like HOL-Analysis).


> This refers to Isabelle/386a31d6d17a.
> An example session is attached.
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171206/c682926d/attachment.bin>

More information about the isabelle-dev mailing list