On Mon, 3 Nov 2014, Timothy Bourke wrote:
* Makarius <makar...@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
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
