[isabelle-dev] sledgehammer response

Tobias Nipkow nipkow at in.tum.de
Sat Aug 31 08:46:22 CEST 2013


When you clicked on the proof generated by sledgehammer in jedit, it would
replace the sledgehammer call in the theory text with the proof, which was
*very* convenient. Alas, that has gone away recently (eg 9228c575d67d). I don't
know if it was intentional or not, the NEWS file does not seem to mention it. In
any case, it would be great to have the old behaviour back.

Tobias


More information about the isabelle-dev mailing list