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

On Tue, 27 May 2014, René Neumann wrote:

`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.
`

`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

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