*To*: cl-isabelle-users at lists.cam.ac.uk, marmsoler_diego at yahoo.it*Subject*: Re: [isabelle] Print proof of theorem*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 31 Oct 2012 20:49:35 +0100*In-reply-to*: <000301cdb29c$311933f0$934b9bd0$@yahoo.it>*Organization*: TU Munich*References*: <000301cdb29c$311933f0$934b9bd0$@yahoo.it>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121011 Thunderbird/16.0.1

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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Print proof of theorem***From:*Diego Marmsoler

- Previous by Date: Re: [isabelle] Converting bool to {0,1}
- Next by Date: Re: [isabelle] Started auction theory toolbox; announcement, next steps, and questions
- Previous by Thread: [isabelle] Print proof of theorem
- Next by Thread: Re: [isabelle] Print proof of theorem
- Cl-isabelle-users October 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list