I don't really mind, and I imagine that there aren't many uses at the moment, so you could get away with it.
On the other hand, it does create an incompatibility between HOL and FOL (and therefore ZF). Larry On 17 Apr 2012, at 07:35, Tobias Nipkow wrote: > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
