Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] LaTeX-Printing: <proof> in excluded sections


view this post on Zulip Email Gateway (Aug 19 2022 at 14:34):

From: René Neumann <rene.neumann@in.tum.de>
Dear list,

I'm currently using Isabelle 2013-2 and trying to prepare a document
with it.

In my theory I have a large section of excluded lemmas, i.e. they are
surrounded by (<) and (>). Unfortunately, in my outline
(document_variants="outline=/proof,/ML"), I still see a large line of
<proof><proof><proof><proof>… stemming from the lemmas in this section.

Is there some way to get rid of them?

Thanks,
René
smime.p7s

view this post on Zulip Email Gateway (Aug 19 2022 at 14:34):

From: Makarius <makarius@sketis.net>
This is a collision of two different concepts here: ad-hoc removal of
source parts via (<) and (>) vs. formal tags around certain command
spans.

It is just one of these "too many modes, too many options" indidents that
they don't work together smoothly. To avoid that, you can try to use just
one variant: formal tags like %invisible for lemma statements with their
proofs.

Makarius


Last updated: Mar 28 2024 at 16:17 UTC