lp15 at cam.ac.uk
Thu May 17 09:27:40 CEST 2012
This does work now, maybe my problem was with the repository version.
On 16 May 2012, at 15:01, Makarius wrote:
> I don't see what you mean. In Isabelle2012-RC2 I can type "sl", wait 300ms, press RETURN, and see sledgehammer running and producing Output incrementally. Then I can click on one of the proposed metis proofs to replace the inlined command by the result -- this was an idea of Alex Krauss to make it work easily without further ado.
More information about the isabelle-dev