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

[Tobias Nipkow]

In HOL, the ASCII syntax for \<longleftrightarrow> is defined to be <-> but
visually <--> would be more appropriate, closer to --> and would also leave room
for an ASCII syntax for \<leftrightarrow> (namely <->).

Any views on such a change?

Tobias