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