Email Gateway (Aug 19 2022 at 12:29): Email Gateway (Aug 19 2022 at 12:29):From: bnord <bnord01@gmail.com>
Hi,
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?
Best Benedikt
Email Gateway (Aug 19 2022 at 12:29):From: Christoph LANGE <math.semantic.web@gmail.com>
2013-11-13 13:14 bnord:
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
Email Gateway (Aug 19 2022 at 12:29):From: bnord <bnord01@gmail.com>
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
Last updated: Apr 19 2024 at 04:17 UTC