Re: [isabelle] document preparation

Am Montag, den 30.06.2014, 18:38 +0200 schrieb Gergely Buday:
> > 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?
> 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?
> - Gergely

Hi Gergely,

You can use (*<*) and (*>*) to hide parts of your theories.



... hidden stuff ...


Another options are command tags, see Section 4.3 in the Isabelle
reference manual.

  lemma X: ...
  proof %invisible (induct x)

 - Johannes

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