*To*: Lars Hupel <hupel at in.tum.de>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Continuing with a proof after a failed 'done'*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 2 Aug 2016 16:46:50 +0200*In-reply-to*: <40a825f7-63b2-a21c-3116-6ace8970a1a9@in.tum.de>*References*: <40a825f7-63b2-a21c-3116-6ace8970a1a9@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

Hi Lars, Just insert a "sorry" after the failing "done" and you can go on. Andreas On 02/08/16 16:36, Lars Hupel wrote:

Dear list, I'm currently working on refactoring a rather large Isar proof. In there, I have a small number of short 'apply' scripts. When these break, I get "Failed to finish proof" as expected on 'done'. However, unlike a failed 'by' proof, I can't continue with the rest of the proof. Consider this small example: lemma assumes P Q shows "P â Q" proof show P by rule next show Q sorry qed Here, the "show Q" part can be checked as normal. However: lemma assumes P Q shows "P â Q" proof show P apply rule done next show Q sorry qed ... everything after 'done' is red. (I guess this counts as a "feature request".) Cheers Lars

**Follow-Ups**:**Re: [isabelle] Continuing with a proof after a failed 'done'***From:*Lars Hupel

**References**:**[isabelle] Continuing with a proof after a failed 'done'***From:*Lars Hupel

- Previous by Date: [isabelle] Continuing with a proof after a failed 'done'
- Next by Date: Re: [isabelle] Continuing with a proof after a failed 'done'
- Previous by Thread: [isabelle] Continuing with a proof after a failed 'done'
- Next by Thread: Re: [isabelle] Continuing with a proof after a failed 'done'
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list