Re: [isabelle] Print proof of theorem

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…



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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