Session ROOT files support 'chapter_definition' entries
General
- Old-style {* verbatim *} tokens have been discontinued (legacy feature since Isabelle2019). INCOMPATIBILITY, use ‹cartouche› syntax instead.
- Session ROOT files support chapter_definition entries (optional). This allows to associate additional information as follows:
- "chapter_definition NAME (GROUPS)" to make all sessions that belong to this chapter members of the given groups
- "chapter_definition NAME description TEXT" to provide a description for presentation purposes
This refers to Isabelle/a9bbf075f431, and AFP/64cf94d5181c provides the following example in thys/ROOT:
chapter_definition AFP (AFP) description " Archive of Formal Proofs "
- Projects
- None
- Subscribers
- None