Re: [isabelle] Remaining reasons for Proof General

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.

On 12/11/13 15:45, Joachim Breitner wrote:
> Hi,
> Am Dienstag, den 12.11.2013, 15:10 +0100 schrieb Manuel Eberl:
>> I must admit I did not know about this option before; it must be rather
>> new. However, the behaviour is… odd. It seems to complete as soon as
>> there is only one alternative left, i.e. "\alp" is turned into "α".
>> "\ta" is turne into "τ". When one types "\alpha", one gets "αha", when
>> one types "\tau", one gets "τu". So basically, if one wants to use this
>> feature, one has to remember what part of the abbreviation will lead to
>> there being only one possibly completion.
> I believe that that will soon enter your procedural memory. I also just
> recently switched on this feature and from time to time write Γma, but
> it becomes less often quickly. With this, entering fancy symbols becomes
> quite nice.
> There is still the problem that it relies on unique completions, and
> some symbols don’t have short unique prefixes, e.g. \sqsubsete is not a
> great win – but then, this symbol has [=, so I just have to get used to
> that.
> Greetings,
> Joachim

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