* Makarius <makar...@sketis.net> [2014-11-03 10:30 +0100]: > On Mon, 3 Nov 2014, Timothy Bourke wrote: > > >* Makarius <makar...@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.
signature.asc
Description: Digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
