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

[Lawrence Paulson]

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.