[isabelle-dev] Abbreviation for \<leftarrow>

[Lars Noschinski]

On 05.03.2014 16:25, Makarius wrote:
> Did you try any of the catch-all abbreviations, like <. for left
> arrows, or .> for right arrows, or <> for double arrows?
No; I only discovered them today. As \<leftarrow> is the only left arrow
I use, this will probably work. Still, having symmetric abbreviations
would be nice.
> Ambiguous completions are never immediate, though.
I never used immediate completion. I need to try again it with the
semantic completion.
> It is also possible to add more abbreviations in
> $ISABELLE_HOME_USER/etc/settings, although I consider that as
> something for expert users only.
I like to keep my settings as close to the default as possible. It is
annoying enough to keep my jEdit configuration in sync between different
Isabelle releases.

  -- Lars