[isabelle-dev] NEWS: uniform document heading commands

[Makarius]

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.


 	Makarius

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