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

[Tobias Nipkow]

Am 17/04/2012 17:56, schrieb Makarius:
> Why then the proposal to change the prover syntax?

What I meant was not just the prover syntax but also the input syntax. In fact,
primarily the input syntax. One could change merely the latter (which is what PG
does), but that introduces an inconsistency: if you type <--> and allow the
editor to change it to \<longleftrightarrow>, you are fine, but if you leave it
in ASCII, it yields a parser error. That is not so nice.

Tobias