Am 17/04/2012 16:27, schrieb Lawrence Paulson: > I think you are right that ASCII syntax is almost completely irrelevant now. > Hardly anybody sees it.
It is relevant as an input method, and that is exactly what my suggestion is about. I am not interested in ASCII art but in a smooth input method. When I type, I would prefer to keep on typing. Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
