Re: [isabelle] New error messages in Isabelle 2013



On Wed, 30 Jan 2013, Alfio Martini wrote:

If I want to proof something (especially in apply-style which sometimes
pre-dates an isar-proof to get some inspiration of what the tools are
able to proof automatically), I really like to only feed command by
command to the prover ("what are the goals exactly after the 'with'",
"what does simp remove/unfold", "what goals does 'induction' give" ...).


I think this point is fundamental with respect to the discussion of the elimination of the output window in the near future.

Just to repeat canonical Isabelle terminology: "old-fashioned" -> "legacy" -> "eliminated". The present state of the output window (for goal states) is "old-fashioned", and there are still more situations than I would like to see, where it is actually needed. It is unlikely to become legacy or eliminated in general, because some tools might always need to print things out of order.


Apply proof scripts are essential for proof exploration and also as mentioned by René above, to the (experimental) understanding of Isabelle automation proof procedures as well .

Back to the very start of this thread. The "more informative error messages for Isar proof commands" from NEWS means that is now easier to write certain structured proofs without peeking at machine states all the time. I did that in practice, when preparing the Isabelle/Isar course at Orleans last October. It worked approx. 90% in these examples. But the participants then had to do it in Isabelle2012 without this convenience of Isabelle2013.


	Makarius


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