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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
