Lars Hupel

2016-08-02 14:41:21 UTC

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

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