*To*: "C. Diekmann" <diekmann at in.tum.de>*Subject*: Re: [isabelle] Verify the legitimacy of a proof?*From*: Makarius <makarius at sketis.net>*Date*: Sat, 8 Jul 2017 16:24:07 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com>*References*: <CADYF24fBE5-wFje-T9-z2c9Um4ZGf1y+ukaSiDi3EPa9uRBEaw@mail.gmail.com> <CAGbqCMxFwASJH4ympZ589fVua9-kX0qs4K-HAb1z5XgSPg2=Bw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.1.1

On 07/07/17 20:27, C. Diekmann wrote: >> That is, I want to ensure that no lemma in the >> proof tree ended with "sorry", > > If you make a command line run with `isabelle build`, every use of `sorry` > is counted as cheating and makes the build fail (but only at the end of the > build, not at the time when the thy with the sorry is processed). > > This raises a new question: can I enable cheating (quick_and_dirty) mode in > a command line build? Like this: isabelle build -o quick_and_dirty Makarius

**References**:**[isabelle] Verify the legitimacy of a proof?***From:*scott constable

**Re: [isabelle] Verify the legitimacy of a proof?***From:*C. Diekmann

- Previous by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Date: Re: [isabelle] Verify the legitimacy of a proof?
- Previous by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Next by Thread: Re: [isabelle] Verify the legitimacy of a proof?
- Cl-isabelle-users July 2017 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