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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
