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

Tobias Nipkow nipkow at in.tum.de
Tue Apr 17 08:35:28 CEST 2012

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?


More information about the isabelle-dev mailing list