[isabelle-dev] NEWS: uniform document heading commands

[Timothy Bourke]

* Makarius <makarius at sketis.net> [2014-11-03 10:30 +0100]:
> On Mon, 3 Nov 2014, Timothy Bourke wrote:
> 
> >* Makarius <makarius at sketis.net> [2014-11-02 20:24 +0100]:
> >>*** Document preparation ***
> >>
> >>* Document headings work uniformly via the commands 'chapter',
> >>'section', 'subsection', 'subsubsection' -- in any context, even
> >>before the initial 'theory' command.
> >
> >Very nice. Thank you.
> >
> >Would it also be reasonable to allow 'text' before an initial 'theory' ?
> 
> I have asked myself that yesterday, when updating some AFP entries in that
> respect.
> 
> The canonical question: Is such a feature really needed?
> 
> So far the standard way is to say 'theory' first, before writing longer
> paragraphs of text.  The concept of Isabelle document preparation is to
> write in a formal context (which is required for antiquotations), but before
> the theory start it is undefined.

I was thinking of the case where one wants to break up a set of
theories into chapters while still keeping each theory within its own
section.

The first theory in a new chapter could now start:

  chapter "Theories A-D"

  section "Theory A"

  theory A imports Main begin ... end

In this case, 'text' would be useful for writing introductory
paragraphs between 'chapter' and 'section'.

But, maybe it is better to dedicate a theory file to new chapters :

  chapter "Theories A-D"

  theory %invisible begin

  text {* ... *}

  end %invisible

And then a top-level 'text' is not needed.

Does anyone else had similar experiences with structuring proof
documents?

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: Digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141103/a6e697cf/attachment.sig>