On Wed, 5 Mar 2014, Lars Noschinski wrote:
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?
As \<leftarrow> is the only left arrow I use, this will probably work.
Still, having symmetric abbreviations would be nice.
Now I also remember why <- is not an abbreviations: for analogy with the
double arrow: <= is important as \<le>, and not an arrow.
I never used immediate completion.
In that case <. with history should do the job. It is just a matter to
know that this odd sequence is active, but it is odd on purpose, to
minimize conflicts with sane notation.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
