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

Lars Noschinski noschinl at in.tum.de
Tue Nov 13 16:59:12 CET 2012

```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
```