[isabelle-dev] Abbreviation for \<leftarrow>
makarius at sketis.net
Wed Mar 5 17:12:29 CET 2014
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.
More information about the isabelle-dev