nipkow at in.tum.de
Mon Sep 2 12:31:31 CEST 2013
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.
- 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
- 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
- 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
Neither is desirable and I thought at least a) was not the case in the past.
More information about the isabelle-dev