Re: [isabelle] Print proof of theorem



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 at 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







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