Re: [isabelle] Build LaTex document without proof checking

On Tue, 22 May 2012, Tobias Nipkow wrote:

There was a "skip proofs" option once, but I suspect that has gone...

Toplevel.skip_proofs is still there as an add-on feature, and it should work in the same way as it ever did, what ever that means.

Am 22/05/2012 08:15, schrieb C. Diekmann:

Unfortunately using 'usedir -D' and working on the generated *.tex files is not an option.

This statement is unproven.

Generally, the document preparation system works in batch mode. There are various tricks to tune the behaviour of batch mode, but no fundamental way to change the way it works until the next big reform of all this.


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