Re: [isabelle] Unwanted content in a session


> 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".


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