On Mon, 4 Jun 2012, Tobias Nipkow wrote:
Isabelle does not allow you to keep on proving a lemma after you have
already proved all subgoals, although it could just ignore further proof
steps, thus saving you the effort to comment them out...
Err, this is exactly what happens in Isabelle/jEdit, due to its recovery
(which is still crude):
lemma True True
proof -
show True ..
show True ..
show True .. -- ignored
show True .. -- ignored
qed
lemma True True
apply (rule TrueI)
apply (rule TrueI)
apply (rule TrueI) -- ignored
apply (rule TrueI) -- ignored
done
Error recovery could be smarter than that, and in particular take the
proof structure into account (based on the indentation of the source).
As I said already on this thread, I've worked a bit with OCaml recently,
and it still has this strict stop-at-first-error policy, which turns out
very awkward.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
