Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Presenting Theories

view this post on Zulip Email Gateway (Aug 18 2022 at 11:32):

From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi

I've got a theory that I wish to print out in pdf form, which uses
Multiset.thy, so has

imports "Multiset"

before the "begin" of the theory file. When I then use isatool make,
the document that comes out has the whole of Multiset.thy before the
markup of my theory file. This even happens if I use the (<)
comments around the

imports "Multiset"

How do I set up the IsaMakefile, or whatever needs to be changed, so
that I only get my theory printed out?

Thanks

Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 11:32):

From: Alexander Krauss <krauss@in.tum.de>
Peter Chapman wrote:

You can add

no_document use_thy "Multiset"

to ROOT.ML, which loads the Multiset theory before your theory, with
document generation switched off.

Alex

view this post on Zulip Email Gateway (Aug 18 2022 at 11:32):

From: Nicole Rauch <rauch@informatik.uni-kl.de>
Hello Peter,

adding the line

no_document use_thy "Multiset";

to the ROOT.ML file that is in the same directory as your theory
should do the trick.

HTH,

Nicole

Last updated: May 03 2024 at 04:19 UTC