[isabelle-dev] Abbreviation for \<leftarrow>
makarius at sketis.net
Mon Apr 7 17:19:09 CEST 2014
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
> 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:
date: Thu Apr 03 15:40:31 2014 +0200
more symbol abbrevs, e.g. relevant for list comprehension in HOL/List.thy
date: Sun Apr 06 19:16:34 2014 +0200
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.
More information about the isabelle-dev