[isabelle-dev] NEWS: session 'document_files'

Tobias Nipkow nipkow at in.tum.de
Sun Apr 13 12:23:03 CEST 2014

That works fine, thank you.


On 11/04/2014 23:52, Makarius wrote:
> On Fri, 11 Apr 2014, Tobias Nipkow wrote:
>> What I sometimes need is to have the latex files generated but not processed.
>> Currently I achieve this with a dummy root.tex file that includes nothing. Is
>> there a less dummy way?
> There is no need for root.tex and latex to produce a dummy root.pdf. This can be
> done more directly via some document/build script that merely does "touch
> root.pdf".  See the included example session.
> That is functionality from the summer 2012 reform, and I am rather glad that the
> number of build options was successfully reduced, while it has become more general.
> If there is a strong need for it, one could add some option to the "isabelle
> mkroot" tool to produce such a setup -- it presently uses only 2 letters of the
> alphabet for options.
>     Makarius

More information about the isabelle-dev mailing list