*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Build LaTex document without proof checking*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 23 May 2012 07:46:16 +0200*In-reply-to*: <alpine.LNX.2.00.1205222311280.26567@macbroy21.informatik.tu-muenchen.de>*References*: <CAGbqCMwKdshYeUoBpCj0=bwdEJ6PcrnmidjnGdr0PvC2YUXTRw@mail.gmail.com> <4FBBF110.5000402@in.tum.de> <alpine.LNX.2.00.1205222311280.26567@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

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

**References**:**[isabelle] Build LaTex document without proof checking***From:*C. Diekmann

**Re: [isabelle] Build LaTex document without proof checking***From:*Tobias Nipkow

**Re: [isabelle] Build LaTex document without proof checking***From:*Makarius

- Previous by Date: Re: [isabelle] RC3 startup problem on Scientific Linux
- Next by Date: Re: [isabelle] Defining Cases for your own custom Datatypes
- Previous by Thread: Re: [isabelle] Build LaTex document without proof checking
- Next by Thread: Re: [isabelle] Build LaTex document without proof checking
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list