> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
