I use “thm” all the time, especially to inspect theorems that are pre-built and therefore not open to inspection via hover-click directly. Larry
> On 15 Apr 2015, at 09:02, Gerwin Klein <gerwin.kl...@nicta.com.au> wrote: > > >> Despite such routine improvements, many users will probably just stick to >> old habits from the TTY age, and put the sledgehammer command into the text. >> (Are there remaining uses of this ancient form? Or are there still pending >> problems with the current Sledgehammer panel?) > > I don’t think such uses of essentially diagnostic commands should go away, > even if the corresponding panel works perfectly. > > I find typing in a diagnostic command usually much faster and less disruptive > of the workflow than finding a panel in a list of tabs, and using the mouse > to move focus there. Even though we have the very nice command-click for > theorems etc, I still find myself using the thm command semi-regularly, just > because I don’t want to pick up the mouse, or I want to leave in the command > to remind myself of something, or I want to see the theorem in the context of > where I’m trying to use it instead of were it is define. > > Sledgehammer is a slightly different case, because it often takes longer, but > even here I still sometimes prefer the text to the graphical interface when > I’m just using it to find a theorem. > > Panels are clearly better for beginners, and I do myself much appreciate them > for things I don’t do often, but I think we should continue to support both > modes of interaction so that people can do what suits their workflow best. > > Cheers, > Gerwin > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
