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



The way I do markup is undoubtedly viewed by some as an abuse of the document preparation system, but I have exactly the same goals as you list below. An example of a paper written in that style can be found here, starting on page 5:

http://www.cl.cam.ac.uk/~lp15/Pages/Gödel-ar.pdf

I didn't understandThe following paragraph, were you wrote about modifying the behaviour of the LaTeX parser. I never do that. Equally there's no need to manually escape anything. The main trick is to let the document preparation system translate your theory files into LaTeX. This is not something you are supposed to do, so the way of doing it seems to change every year or two.

Larry Paulson


On 7 Oct 2013, at 18:46, Christoph LANGE <math.semantic.web at gmail.com> wrote:

> Thanks, Larry and Tobias, for sharing your experience on including
> Isabelle sources in LaTeX.  I see that one has more flexibility in using
> the document preparation system than I had thought.
> 
> Nevertheless I wonder whether is also offers an easy solution for the
> problem that I tried to solve with my pmisabelle.sty, i.e. a solution
> that addresses the following requirements:
> 
> My papers consist of a lot of LaTeX and a few short Isabelle listings;
> therefore:
> 
> 1. I'd like to write them in my favourite LaTeX editor.
> 2. They sometimes deviate from my actual formalisation for readability
> or didactic purposes.
> 3. It is not absolutely essential that these listings are syntactically
> and semantically correct.  "Correct to the eye of a proof-reader" is
> good enough; "correct to Isabelle's verification engine" is nice to have
> but not essential.
> 4. Exporting LaTeX snippets from my actual Isabelle sources is merely
> nice to have.  I wouldn't mind copy/pasting snippets from my *.thy files
> into the LaTeX editor and applying minor adaptations manually or via a
> script to make them render as nice LaTeX.
> 5. I don't want to invest a lot into the formalisation (such as
> inserting special markup) to make it "exportable".





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