Email Gateway (Aug 19 2022 at 08:53): Email Gateway (Aug 19 2022 at 08:53):From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
For my Master's thesis, I had some success using the technique suggested
by this page:
https://isabelle.in.tum.de/community/Generate_TeX_Snippets
Tim
<><
signature.asc
Email Gateway (Aug 19 2022 at 08:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Diego,
I'm rather new to Isabelle and I'm currently writing my Master's Thesis
using Isabelle/Isar and the document preparation system. I was wondering if
there is a way to print out a theorem with its proof using antiquotations of
the Isabelle document preparation system.
there are indeed no antiquotations to refer to whole blocks of Isar text.
I'm asking because what I want is
to hide the proofs initially and show only the theorems and put the proofs
then in the appendix at the end of the document.
What might help in your case is to tag lemma statements with command
tags and produce different variants of documents which are then glued
together in a suitable way by latex. See »Markup via command tags« in
the Isar reference manual.
Do not hesitate to ask further if this sounds to obscure…
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:05):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
Hi to all,
I'm rather new to Isabelle and I'm currently writing my Master's Thesis
using Isabelle/Isar and the document preparation system. I was wondering if
there is a way to print out a theorem with its proof using antiquotations of
the Isabelle document preparation system. I'm asking because what I want is
to hide the proofs initially and show only the theorems and put the proofs
then in the appendix at the end of the document.
Thanks.
Diego
Email Gateway (Aug 19 2022 at 09:05):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
Hi, Florian,
I solved my problem using TeX_Snippeds as suggested in:
https://isabelle.in.tum.de/community/Generate_TeX_Snippets
However I will consider your advice to use "Command Tags" as well. Maybe it
can be used to solve the problem in a nicer way.
Anyway, thanks for your advice.
Cheers,
Diego
From: Florian Haftmann [mailto:florian.haftmann@informatik.tu-muenchen.de]
From:
Hi Diego,
I'm rather new to Isabelle and I'm currently writing my Master's
Thesis using Isabelle/Isar and the document preparation system. I was
wondering if there is a way to print out a theorem with its proof
using antiquotations of the Isabelle document preparation system.
there are indeed no antiquotations to refer to whole blocks of Isar text.
I'm asking because what I want is
to hide the proofs initially and show only the theorems and put the
proofs then in the appendix at the end of the document.
What might help in your case is to tag lemma statements with command tags
and produce different va
riants of documents which are then glued together in a suitable way by
latex. See >Markup via com
mand tags< in the Isar reference manual.
Do not hesitate to ask further if this sounds to obscure.
Cheers,
Florian
--
PGP available:http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_infor
matik_tu_muenchen_de
Email Gateway (Aug 19 2022 at 09:24):From: Diego Marmsoler <marmsoler_diego@yahoo.it>
Works perfectly fine!
Thanks.
Diego
From: Tim (McKenzie) Makarios [mailto:tjm1983@gmail.com]
For my Master's thesis, I had some success using the technique suggested
by this page:https://isab
elle.in.tum.de/community/Generate_TeX_Snippets
Tim
<><
Last updated: Apr 19 2024 at 04:17 UTC