*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Build LaTex document without proof checking*From*: "C. Diekmann" <diekmann at in.tum.de>*Date*: Wed, 23 May 2012 13:27:28 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*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>*Sender*: c.diekmann at googlemail.com

On 2012/5/22 Makarius wrote: > 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. Thank you, that is exactly what I was looking for. An explanation how to use this feature is already in the mailing list. On Fri, 11 Feb 2011 16:16:11 Brian Huffman wrote: >You can speed things up a bit by running Isabelle in "skip proofs" >mode. Try adding commands to set the following two references before >"use_thys" in ROOT.ML: > >quick_and_dirty := true; >Toplevel.skip_proofs := true; >use_thys ["MyTheory"]; Regards Cornelius

**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] jEdit: cursor movement and goal display
- Next by Date: Re: [isabelle] jEdit: cursor movement and goal display
- Previous by Thread: Re: [isabelle] Build LaTex document without proof checking
- Next by Thread: [isabelle] naming facts
- 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