[isabelle-dev] jedit

Lawrence Paulson 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.
Larry

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 mailing list