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