HomeIsabelle/Phabricator
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
  "
Written by makarius on Aug 27 2022, 10:08 PM.
User
Projects
None
Subscribers
None

Event Timeline