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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
