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.

Right, I forgot about 'qed'. This one is not as easy to work around
using a single strategically placed 'sorry'.




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