Re: [isabelle] Print proof of theorem

Hi, Florian,

I solved my problem using TeX_Snippeds as suggested in:

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.


> From: Florian Haftmann [mailto:florian.haftmann at]
>> 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:

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