*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*: Tue, 22 May 2012 22:03:28 +0200*In-reply-to*: <CAGbqCMwKdshYeUoBpCj0=bwdEJ6PcrnmidjnGdr0PvC2YUXTRw@mail.gmail.com>*References*: <CAGbqCMwKdshYeUoBpCj0=bwdEJ6PcrnmidjnGdr0PvC2YUXTRw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:12.0) Gecko/20120428 Thunderbird/12.0.1

There was a "skip proofs" option once, but I suspect that has gone... Tobias Am 22/05/2012 08:15, schrieb C. Diekmann: > Hello, > > I am creating a pdf document from my isabelle theory, using 'isabelle > make -B' to rebuild the pdf document. Unfortunately, this takes very > long. Is it possible (during development) to disable the proof > checking? Most of my text in the *.thy files is enclosed in text {* *} > blocks. I make heavy use of 'thm' to refer to the definitions. > Unfortunately using 'usedir -D' and working on the generated *.tex files > is not an option. It would be great to see how changes in the *.thy file > end up in the resulting pdf. > > > Best Regards > Cornelius Diekmann

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

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

- Previous by Date: Re: [isabelle] RC3 startup problem on Scientific Linux
- Next by Date: [isabelle] Defining Cases for your own custom Datatypes
- Previous by Thread: [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