Re: [isabelle] document preparation: folding inside ignored parts

On Sat, 27 Jun 2015, Bertram Felgenhauer via Cl-isabelle-users wrote:

I've encountered an oddity in Isabelle's (2015) document preparation.
I have a theory with some boring facts that I want to hide from the
generated documents, so I'm using (*<*)/(*>*) like this:

 lemma some_boring_lemma: "1+2 = 3"
 by simp

This works as expected (no output is produced for this lemma nor its
proof) by default. But if proofs are folded (e.g. using the recipe for
outlines from the tutorial), then the folded proof appears in the
generated outline, despite belonging to the ignored material.

This is a conflict of features: the older (*<*)(*>*) pseudo-comments (from 2000) don't work together with the newer concept of "tags" (from 2005); note that a proof has such a default %"proof" tag and can thus be folded.

You can try to use just the tag concept alone, notably with annotations like this:

  lemma %invisible boring
    by simp

There are slightly different rules for whitespace handling, but that is a black art in any case.


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