[isabelle-dev] <-> and <-->
Lawrence Paulson
lp15 at cam.ac.uk
Tue Apr 17 09:38:29 CEST 2012
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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
More information about the isabelle-dev
mailing list