[isabelle-dev] sledgehammer response

[Tobias Nipkow]

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