[isabelle-dev] NEWS: uniform document heading commands
hoelzl at in.tum.de
Mon Nov 3 10:47:31 CET 2014
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
> 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
More information about the isabelle-dev