Email Gateway (Aug 19 2022 at 14:39): Email Gateway (Aug 19 2022 at 14:39):From: Gergely Buday <gbuday@gmail.com>
Hi,
I called
isabelle mkroot -d
and then put MyTheory into the file ROOT. Upon
isabelle build -D .
I got an empty root.pdf in output/document, having the title and
Contents. What else should I do so that my theory would appear in the
output? document/root.tex has
\input{session}
Email Gateway (Aug 19 2022 at 14:40):From: Gergely Buday <gbuday@gmail.com>
The problem was in ROOT where I put my theory name into the first
theories section with [document=false].
This leads to another question: now everything from the theory is
typeset. Can I suppress parts, or there is another way to typeset only
needed parts?
Email Gateway (Aug 19 2022 at 14:40):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Gergely,
You can use (<) and (>) to hide parts of your theories.
Like:
(<)
... hidden stuff ...
(>)
Another options are command tags, see Section 4.3 in the Isabelle
reference manual.
lemma X: ...
proof %invisible (induct x)
...
qed
Last updated: Apr 24 2024 at 20:16 UTC