[isabelle-dev] sledgehammer response
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
[isabelle-dev] sledgehammer
Please disregard my previous email. I see that there is now a sledeghammer panel (with some more goodies) which avoids having to type sle... and thus solves the issue. Thanks for that Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer
It doesn't always work in the panel either. Some lurking bugs maybe. I'm not sure what you are allowed to do while sh is running. Larry On 31 Aug 2013, at 09:04, Tobias Nipkow nip...@in.tum.de wrote: Please disregard my previous email. I see that there is now a sledeghammer panel (with some more goodies) which avoids having to type sle... and thus solves the issue. Thanks for that Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
