On Mon, 2 Sep 2013, Tobias Nipkow wrote:
Am 02/09/2013 11:18, schrieb Makarius:
The sledgehammer panel has had only 1-2 rounds of refinements so far, and more
precise observations by testers on this mailing list will be required to make it
work smoothly for the coming release.
Some observations:
- When clicking on the generated proof it is appended to the end of the proof
text preceding the invocation point. It would be better to insert a newline
first - otherwise the proof develops in a horizontal rather than the standard
vertical direction.
- Sometimes I click on the generated proof and it is not pasted into the theory
text. It just doesn't work, even if I click repeatedly. I cannot reproduce this
reliably.
- Once one has clicked on a proposed proof and it has been pasted into the
theory window, this does two things:
a) it stops the rest of the running atps.
b) it disables all the proposed proofs, i.e. no more click-and-paste for any
of them.
Neither is desirable and I thought at least a) was not the case in the past.
All of that has improved in Isabelle/08721d7b2262 (and its vicinity).
I've made some fine-tuning without fundamental changes to how it all
works. Lets see if this is sufficient for the release.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
