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
This archive was generated by a fusion of
Pipermail (Mailman edition) and