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