Re: [isabelle] Verify the legitimacy of a proof?



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




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