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



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.