Email Gateway (Aug 18 2022 at 10:04): Email Gateway (Aug 18 2022 at 10:04):From: Martin Klebermaß <martin@klebermass.de>
Hello,
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.
Es grüßt Sie freundlich/best regards,
Martin Klebermaß
============================
martin@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
============================
smime.p7s
Email Gateway (Aug 18 2022 at 10:04):From: Lawrence Paulson <lp15@cam.ac.uk>
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
cleanTeX.pl
Email Gateway (Aug 18 2022 at 10:04):From: Martin Klebermaß <martin@klebermass.de>
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@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
============================
smime.p7s
Email Gateway (Aug 18 2022 at 10:05):From: Martin Klebermaß <martin@klebermass.de>
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@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
============================
smime.p7s
Email Gateway (Aug 18 2022 at 10:05):From: Steven Obua <obua@in.tum.de>
No, you are not the only one, I prefer to use Latex for my papers, too.
It would be good to have a little bit more support for this style of
authoring.
Steven
Email Gateway (Aug 18 2022 at 10:05):From: Makarius <makarius@sketis.net>
There are many ways to be creative here. First of all, see chapter 2 of
the Isabelle System manual for basic explanations of the Isabelle document
tool chain. The default setup (e.g. the one produced via isatool mkdir)
gives Isabelle most of the control. Things can be easily adjusted, e.g.
using the -D option for usedir to dump tex sources separately, potentially
with -d false to disable Isabelle document processing.
While it is most natural to generate the main sources from Isabelle
theories, afterwards it is up to root.tex to assemble all this,
potentially with funny \input{MyTheory.tex} etc. in any way you like.
Concerning the content, you may easily remap Isabelle symbols or tagged
regions using LaTeX macros (see the documentation).
For the really creative user, Isabelle antiquotations written in ML
(depending on the logical context!) may produce formal output quite
easily. (The LaTeX Sugar manual covers advanced use of existing
antiquotations.)
Makarius
Email Gateway (Aug 18 2022 at 10:05):From: Maria Spichkova <spichkov@in.tum.de>
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@in.tum.de
Phone: +49 (89) 289-17882
Fax: +49 (89) 289-17307
Room: 00.09.059
Martin Klebermaß schrieb:
Last updated: May 03 2024 at 12:27 UTC