[isabelle-dev] Deprecating legacy ASCII symbols?

[Jasmin Blanchette]

> Concerning :: versus \<Colon> I am in favour to get rid of \<Colon> altogether: there is visually no difference in final LaTeX documents, and in the editor it introduces a bit too much complication to my taste.

As far as I am concerned: By all means, kill it!

At some point in 2014, I realized \<Colon> only made my life more miserable and stopped using it.

Jasmin