[isabelle-dev] Abbreviation for \<leftarrow>

[Makarius]

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