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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
