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.

Andreas

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.

Cheers
Lars





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