[isabelle-dev] Abbreviation for \<leftarrow>

[Makarius]

On Wed, 5 Mar 2014, Makarius wrote:

> On Wed, 5 Mar 2014, Lars Noschinski wrote:
>
>>  it would be nice if we could also get "<-" as abbreviation for
>>  \<leftarrow> (and probably <-- for \<longleftarrow) by default.
>>  \<leftarrow> is regularly used in Monad syntax and list comprehensions and
>>  it would be nice to have the abbreviations matching the
>>  rightarrow-variants.
>
> I can't say on the spot how it would work out: the current scheme is the 
> result of intensive experimentation over some weeks last summer. This needs 
> to be repeated soon, when the semantic completion is fully operational. 
> Right now I am reworking again some details of that.

The formal conclusion of this thread is two-fold:

changeset:   56380:c771f0fe28d1
user:        wenzelm
date:        Thu Apr 03 15:40:31 2014 +0200
files:       etc/symbols
description:
more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy 
or HOL/Library/Monad_Syntax.thy;

changeset:   56443:ee0f7cfb7bba
user:        wenzelm
date:        Sun Apr 06 19:16:34 2014 +0200
files:       etc/symbols
description:
removed abbrev "<-" again (see c771f0fe28d1) due to conflict with 
important "<->" and "<-->";


So the canonical approach remains "<." with its high ambiguity and 
explicit popup, but this is no problem here.


 	Makarius