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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
