[isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs

[Lars Noschinski]

Hi,

sometimes, I am encountering some erraneous behaviour of qed when a 
structured proof contains some facts for which the final "by" step failed.

Before the closing block the output buffer reads:

   goal:
   No subgoals!

But qed then fails with an error message:

Failed to finish proof:
goal (4 subgoals):
{(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG
  1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) 
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, 
x)})))), fst, snd))
  2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) 
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, 
x)})))), fst, snd))
  3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) 
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, 
x)})))), fst, snd))
  4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) 
(insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, 
x)})))), fst, snd))

The subgoals in this message are the remaining goals of a failed 
qed-step earlier in this proof.

No minimal example yet, I might be able to produce one later this week, 
if Makarius does not already now what happens here.

   -- Lars