[isabelle-dev] NEWS: Z3 open source

[Gerwin Klein]

> 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.