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.


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