Re: [isabelle] Presenting theories without running a session

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.


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