Re: [isabelle] Presenting Theories
Peter Chapman wrote:
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.
You can add
no_document use_thy "Multiset"
to ROOT.ML, which loads the Multiset theory before your theory, with
document generation switched off.
This archive was generated by a fusion of
Pipermail (Mailman edition) and