[isabelle-dev] NEWS: uniform document heading commands

[Johannes Hölzl]

Am Montag, den 03.11.2014, 10:30 +0100 schrieb Makarius:
> On Mon, 3 Nov 2014, Timothy Bourke wrote:

> > 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.

In most cases I want to write a small (informal) introduction. But then
the "theory ... imports ... begin" command looks out of place in the
generated document and I hide it using (*<*) (*>*).

So having a way to write an abstract / or an informal introduction would
be nice.

 - Johannes