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
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.
