[isabelle-dev] Redundant equations in function declarations

[Makarius]

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