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



> 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?

One question answered, one not answered, one new problem ;-)

Cheers,
  Cornelius



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