Re: [isabelle-dev] New proof method "rewrite"
On 14.04.2015 15:59, Lars Noschinski wrote: > Currently, I'm still contemplating whether it is feasible to add a > proper ML interface in the short remaining time, but this probably > needs to wait for the next release, too. Turns out, a proper ML interface is not too hard, see now ef4fe30e9ef1. Writing the patterns down, however, is a quite annoying task. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Z3 open source
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 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
Re: [isabelle-dev] NEWS: Z3 open source
> 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
