Re: [isabelle] 2013-1-RC1: proof method suggested try or try0 no longer overwrites 'try' keyword
On Fri, 4 Oct 2013, Christoph LANGE wrote:
2013-10-03 20:04 Christoph LANGE:
in Isabelle 2013 when I wrote "statement try", or try0, and try found a
proof, clicking on this proof in the output panel replaced the "try"
keyword in the edited source by the proof. This is no longer the case
in 2013-1-RC1. Instead the proof (e.g. "by blast") is placed after the
"try", which remains.
After some more playing I'm starting to realise that this might be a
_feature_. Suppose you try to prove something with Sledgehammer, and it
suggests several possibilities, which you would then minimise, all
possibilities are retained in the document until you finally decide for
one proof. However you would have to clean up yourself all those
alternatives you don't like.
There is indeed a slight change of the behaviour in "sendback" text
produced by commands like sledgehammer, nitpick, try0 etc. Before
Isabelle2013-1 there was no specific support for what is now called "query
operation", and there were some temporarary approximations to a workflow
where you insert commands in the buffer and get them replaced eventually.
With the implicit "auto sledgehammer" and explicit "slegdehammer panel"
you normally don't put query commands in the buffer anymore, and the
editing behaviour has been adapted accordingly. Thus you gain a lot, but
you loose a little bit with commands that still don't have their own query
panel, such as 'try0'. (Supporting both the old and the current behaviour
turned out to lead in an unmaintainable confusion of the code, which would
inevitably lead to bad system rather soon.)
Looking ahead even a bit further, the next stage is to support more
structured editing of the text with assistance by the prover and the
editor. Then the replacement policies would be determined by the text
itself, not funny properties in the sendback messages we still see today.
This archive was generated by a fusion of
Pipermail (Mailman edition) and