Re: [isabelle] Embeding theories in existing latex document



Thank you,

so, copy & paste is the only way?
Would be nice to see someday some generation of macros to access the definitions (eg to insert just something like \isabelle_text{ @{thm mytheorem} }.

For the moment i will use copy and paste then :-)


Es grüßt Sie freundlich/best regards,
	Martin Klebermaß

============================
martin at klebermass.de
============================
Schweiz:
Tramstr. 107
CH-5034 Suhr

Deutschland:
Fuchsbergstr. 11
D-82223 Eichenau

Mobil(DE): +49 (0) 176 / 70073282
Telefon(DE): +49 (0) 8141 / 509040
Mobil(CH): +41 (0) 79 / 7870352
Telefon(CH): +41 (0) 32 / 5107586

============================





Am 18.01.2007 um 12:58 schrieb Lawrence Paulson:

I do this all the time. You just have to grab the generated TeX output and insert it into your TeX file, within the brackets \begin {isabelle}...\end{isabelle} or \isa{...}.

The generated TeX is verbose because it refers to virtually all symbols via macros. I attach a Perl script that replaces these macros by the corresponding characters.

If you want to edit this TeX further, I advise you to use a TeX gui (such as TeXShop) that maps between the typeset output and the corresponding place in the source.

All of this is completely unsupported. I seem to be the only person who wants to write papers directly in LaTeX rather than using Isabelle markup.

Larry


On 18 Jan 2007, at 11:47, Martin Klebermaß wrote:

i have a separate latex document where i want to present my theories, and want to extract some of the definitions and proofs out of my isabelle scripts and embed them into my document.

Is this somehow possible. I have only seen it the other way round embedding latex code into the isabelle documents.

<cleanTeX.pl>

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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