Re: [isabelle] Remaining reasons for Proof General



Maybe I'm to stupid.

I find the "not" case still unpleasant.
- I can't use "~<TAB>" because it's a composing key so I have to type "~<space>C-b<TAB>"
- "\not" is not unique so have to also press Tab

Benedikt

Am 12.11.13 16:02, schrieb Makarius:
On Tue, 12 Nov 2013, Manuel Eberl wrote:

Another problem are codes such as "not", which are still not replaced at
all, since "notation", "note" and so on also exist. I'm afraid I don't
think I can get used to this.

Have you actually tried Isabelle2013-1 already?

It requires some time to study the NEWS and the corresponding documentatation (the jedit) manual. And then make a fresh start into this 4th generation Prover IDE implementation.


    Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.