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