Re: [isabelle] Continuing with a proof after a failed 'done'

Hi Lars,

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:
Hi Andreas,

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 MHonArc.