Re: [isabelle] Presenting Theories
I've got a theory that I wish to print out in pdf form, which uses
Multiset.thy, so has
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
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