Email Gateway (Aug 19 2022 at 14:34): 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
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: Nov 21 2024 at 12:39 UTC