Re: [isabelle] Remaining reasons for Proof General


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


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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