Re: [isabelle] [Isabelle2013-1] try0/try/sledgehammer command isn't replaced when clicking on suggested method.



Guessed so. Thanks.

is there a way to invoke the sledgehammer panel using some keyboard shortcut, ideally such that it becomes visible when there is a result and switches back to the previous panel when selecting some suggestion?

Best Benedikt


Am 13.11.13 14:19, schrieb Christoph LANGE:
2013-11-13 13:14 bnord:
in Isabelle2013-1 on OS X

typing

lemma True try0

and then clicking on the suggested "by simp" yields

lemma True try0 by simp

instead of

lemma True by simp

as in Isabelle2013. It's the same for try/sledgehammer.

Is this intended?
There was an earlier conversation about this, in which I first
complained but then found out that it's actually sometimes useful (at
least with sledgehammer), and Makarius also commented on it.  The thread
starts here:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-October/thread.html#00013
(2013-1-RC1: proof method suggested try or try0 no longer overwrites
'try' keyword)

Cheers,

Christoph






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.