Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?
On 8/27/2012 4:21 PM, Makarius wrote:
I don't think it would be a good idea to introduce aliases for
existing commands, especially very short ones. If you want to be fast
in typing it is better to figure out some jEdit plugins that do the
job. The Sidekick completion is already there; it has some plugin
options to make it more aggressive. Other plugins like superabbrevs
or yet unknown ones might do even more for you.
It was only about style. Some keywords I like or don't mind, but "oops"
and "sorry" don't quite fit in. It's not a problem because I don't think
I'll be postponing or abandoning proofs much in the documents I give
people, and I can strip some things out.
I was going to make a feeble appeal for freedom of keyword syntax,
similar to how we have freedom of notation with Isar, but I decided it's
the standardized keywords that give the language a common feel from
document to document. If you were to let people redefine keywords, there
would be major fragmentation of the language, which would make the
language harder to learn, and you would get blamed for it.
Line noise that is hacked into the computer is better not stored in
the text you produce, unless you never want anyone to read it,
maintain it, work with it elsewise.
Some people have come up with proof languages based on single letter
commands, or even non-letter commands in the spirit of APL. I am fond
of typing fast, but not of reading what looks like mouse droppings on
Readability is huge with me, but it takes a lot of experimenting to find
the balance between using brevity for clarity, and using verboseness for
This archive was generated by a fusion of
Pipermail (Mailman edition) and