[isabelle-dev] NEWS: Session ROOT files support 'chapter_definition' entries, e.g. in AFP/thys/ROOT

Makarius makarius at sketis.net
Sat Aug 27 22:11:22 CEST 2022

*** General ***

* 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

Thus AFP ROOT files can do away with the slightly odd redundancy of "chapter 
AFP session NAME (AFP) ...".

I did not change anything, though, because I reckon that AFP submission tools 
and documentation need to be adjusted as well.


More information about the isabelle-dev mailing list