Re: [isabelle] Continuing with a proof after a failed 'done'
Neither do I understand why they behave differently. Probably only Makarius knows. The
short forms "." and ".." also behave like done and differently from their long forms "by
this" and "by rule". It looks like "by" is the outsider, because "proof(rule) qed" does
not close the proof block, either.
On 02/08/16 16:48, Lars Hupel wrote:
Just insert a "sorry" after the failing "done" and you can go on.
of course, that's a possibility, but I don't understand why 'done' and
'by' behave differently there in the first place.
This archive was generated by a fusion of
Pipermail (Mailman edition) and