[isabelle-dev] sledgehammer

[Makarius]

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