Re: [isabelle] Message output in Isabelle2014 and Isabelle2015



But this would also mean that one does not see the intermediate goal state if something goes wrong in the terminal method slot of by.

lemma "P (xs :: 'a list)"
  by (induct xs) auto

This is more useful when repairing existing proofs, rather than writing new proofs, though.

Dmitriy

On 23.06.2015 15:14, Larry Paulson wrote:
Yes â this might be OK.
Larry

On 23 Jun 2015, at 13:42, Peter Lammich <lammich at in.tum.de> wrote:

One solution that does not involve too much implementation effort might
be to not include the goal-state into the error message, and output this
shorter error message *before* the goal-state.

While the user is typing, he would see a short error message that he
could ignore, followed by the goal state.
When the user is inspecting the (error-)result of the command, he would
see the error message first. Warnings should still be printed after the
goal-state







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.