[isabelle-dev] NEWS: uniform document heading commands

Makarius makarius at sketis.net
Mon Nov 3 10:30:10 CET 2014

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 

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.


                   http://stop-ttip.org  777,460 people so far

More information about the isabelle-dev mailing list