[isabelle-dev] Deprecating legacy ASCII symbols?
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