Re: [isabelle] Unwanted content in a session



Mark,

> I have a theory , Zed, that imports While_Combinator.
> When I generate a session that includes Zed.thy, the generated
> document.pdf includes a section generated from While_Combinator.thy.
> 
> I don't want that section. Is there some way to keep it from being
> generated?

Edit the file ROOT.ML in the session directory and add a line:

  no_document use_thy "While_Combinator";

before the line for "Zed".



Alex.





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