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.
On 23.06.2015 15:14, Larry Paulson wrote:
Yes â this might be OK.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and