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.

Like:

(*<*)

... hidden stuff ...

(*>*)

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

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


 - Johannes





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