[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