Re: [isabelle] Presenting Theories

Hello Peter,

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?

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.



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