[isabelle-dev] <-> and <-->

[Tobias Nipkow]

Am 18/04/2012 04:23, schrieb Christian Sternagel:
> +1 for <--> (since it would agree, as Tobias pointed out, with the established
> =>, ==>, ->, -->).

Thanks for actually referring to the topic at hand. The discussion has gotten
completely off topic and became quite fundamentalist. I was merely suggesting to
improve the internal consistency of our ASCII arrow notation schemes (and
consistency with other editors like TeXmacs, as I later realised). For me this
is an abstract issue that is independent of any editor. In particular, I did not
want to discuss the merits of different editors.

Since it is a minor issue and got little support, I will not pursue the idea.

Tobias