[isabelle-dev] Deprecating legacy ASCII symbols?

Jasmin Blanchette jasmin.blanchette at inria.fr
Tue Jun 30 17:43:19 CEST 2015

> 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.


More information about the isabelle-dev mailing list