Re: [isabelle-dev] jedit

[Lawrence Paulson]

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.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Codegen and generic numerals

[Makarius]

Another fine point that showed up in Isabelle2012-RC2 last Monday:

lemma 1 + 1 = 2 by simp  -- works

value 1 + 1  -- (1∷'a) + (1∷'a)
value [1] = [2]  -- equal_class.equal (1∷'a) ((1∷'a) + (1∷'a))

This is all correct, but maybe a bit unexpected for users.


Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev