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 ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and