Re: [isabelle] Poor man's LaTeX markup for Isabelle listings



Am 07/10/2013 17:15, schrieb Lawrence Paulson:
> Some people use this system to write entire papers based upon their theory development. But this isn't very practical if your development takes 40 minutes to run, as in a recent one I completed.

Are saying you need to run the whole development every time you latex your
paper? This is only the case if you want to include literally (some of) the text
of your theories. Which doesn't work very well anyway because you have to stick
to the order in which the material is presented in the theories.

The normal way to write a paper with Isabelle is to build on an image that
contains all the theories, start from that image and use antiquotation to
display material.

If for formatting reasons you absolutely need some fragment of the source text,
the LaTeX sugar document contains a section Theory Snippets describing how to do
that in a selective manner.

Tobias




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