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

Tobias Nipkow nipkow at in.tum.de
Tue Apr 17 18:45:42 CEST 2012

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.


More information about the isabelle-dev mailing list