[isabelle-dev] sledgehammer

[Tobias Nipkow]

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.

Tobias