Email Gateway (Aug 22 2022 at 10:23): Email Gateway (Aug 22 2022 at 10:23):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
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.
Cheers,
Bertram
P.S. I started with ROOT and root.tex as generated by isabell mkroot -d,
and then modified the ROOT file as follows:
session "doctest" = "HOL" +
options [document = pdf, document_output = "output", document_variants="document:outline=/proof,/ML"]
theories
Scratch
document_files
"root.tex"
Email Gateway (Aug 22 2022 at 10:23):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC