Re: [isabelle] Presenting theories without running a session

On Sun, Feb 13, 2011 at 2:22 PM, Makarius <makarius at> wrote:
> On Thu, 10 Feb 2011, Robert Lamar wrote:
>> I am curious about converting .thy files to .tex files without running a
>> session to verify the document (with Isabelle 2011).  Is this possible?
>> I have been looking at the documentation for 'isabelle make', 'isabelle
>> usedir', 'isabelle document', and 'isabelle latex', but I cannot
>> conclude if producing LaTeX code depends on processing the documents,
>> producing the heap, and so on.
> The main idea behind the Isabelle document preparation system is to
> produce a pinted "proof" of your formal development, using standard
> typesetting technology.  This explains some biases towards properly
> checked sources, although there are numerous ways to print anything you
> want, rearrange the order of theories etc.  There are open-ended
> possibilities that some users have turned this into an art in itself.
> There are alternative ways to make simple draft printouts of the sources,
> notable the 'display_drafs' command (the the isar-ref manual) or the
> standard File/Print operation of Isabelle/jEdit.  The latter works
> surpringly well together with the IsabelleText font.

Thank you very much for these pointers. I will give them a closer look.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.