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?
Am 13.11.13 14:19, schrieb Christoph LANGE:
2013-11-13 13:14 bnord:
in Isabelle2013-1 on OS X
lemma True try0
and then clicking on the suggested "by simp" yields
lemma True try0 by simp
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
(2013-1-RC1: proof method suggested try or try0 no longer overwrites
This archive was generated by a fusion of
Pipermail (Mailman edition) and