Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unwanted content in a session

Email Gateway (Aug 18 2022 at 10:17):

From: "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>
All -

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?

Thanks - Mark Janney

Email Gateway (Aug 18 2022 at 10:17):

From: Alexander Krauss <krauss@in.tum.de>
Mark,

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.

Last updated: May 03 2024 at 08:18 UTC