# [isabelle] Continuing with a proof after a failed 'done'

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Continuing with a proof after a failed 'done'
*From*: Lars Hupel <hupel at in.tum.de>
*Date*: Tue, 2 Aug 2016 16:36:35 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

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

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