# Re: [isabelle] Embeding theories in existing latex document

well thats not exactly what i want ;)

but Lawrence Paulsons tip gave me a new idea for a better hack.

I will set up a presentation theorem just containing entrys like

text_raw{*
\newcommand\mylemma{
@{thm mylemma}
}
*}


In the generated theorem file i have to remove the generated headers and footers after that i can use \mylemma in my text. (I have tested this now with one example theorem. I will see if it works with all my lemmas)


Not the perfekt solution, but i think the best one at the moment to get.

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 13:25 schrieb Maria Spichkova:


Using "isatool make" you will get separate TeX-File for each theory, such, you can also use TeXcommand to insert the TeX-version of your theory in the main file:

\input{mytheorem}

Schöne Grüsse,
Maria

-----------------------------------------
Maria Spichkova
Institut für Informatik
Technische Universität München
Boltzmannstr. 3
D-85748 Garching
Germany

Email: spichkov at in.tum.de
Phone:  +49 (89) 289-17882
Fax:  +49 (89) 289-17307
Room:  00.09.059

Martin Klebermaß schrieb:

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.