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

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.

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





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