On Fri, 25 Jul 2014, Gerwin Klein wrote:
On 25 Jul 2014, at 10:23 am, Makarius <makar...@sketis.net> wrote:
Oddly, people are still seen using 'find_theorems' etc. inlined into the source
text. That was an intermediate approach from several years ago. If it is still
used today, what are the remaining resons for it?
Not having to touch the mouse is the main reason for me why I still use
thm, find_theorems, sledgehammer etc commands.
Does that actually refer to Isabelle2014-RC0, or some older version?
I have reworked the focus handling such that the panels that require some
input move the focus in the right spot. It should be also possible to
define some keyboard shotcurts to activate the panel in question.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
