[isabelle-dev] Deprecating legacy ASCII symbols?

[Makarius]

On Tue, 30 Jun 2015, Jasmin Blanchette wrote:

> This apparatus is rather heavy on beginners, and even experts will 
> sometimes pause for a second to wonder whether they want to type :: or 
> \<Colon> or whatever. I suspect one reason why John Harrison is so fast 
> is that in HOL Light you don’t have to make such trivial decisions all 
> the time.

You are probably right about John Harrison and HOL-Light.

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.

The special \<Colon> symbol goes back to a request from David von Oheimb, 
when he still maintained the so-called 8bit package, i.e. the non-ASCII 
mode before the classic X-Symbol package of Proof General 2.x.


 	Makarius