Re: [isabelle] Build LaTex document without proof checking



Am 22/05/2012 23:16, schrieb Makarius:
> 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.

Thanks for the correction. I was not sure.

Tobias

> 
>> 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.
> 
> 
>     Makarius





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