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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
