As regards motivation, remember, back then it was a thing of beauty. I could easily remember the day when it was possible to use lowercase letters.
I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. Even on my MacBook where the Unicode characters are off by one (I wish I could fix this), I have been using symbolic identifiers because I know that my main work will be done on machines without that bug. Larry On 17 Apr 2012, at 15:13, Makarius wrote: > A brief look at the history and source archive shows that this ASCII art has > already been there since Isabelle86. Larry might still remember his > motivations in the depths of time. I've always understood <-> as "visually > appropriate" counterpart of --> in the sense of the physical length, despite > the optical distortion since ASCII < > are not proper arrow heads. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
