[isabelle-dev] Deprecating legacy ASCII symbols?
makarius at sketis.net
Tue Jun 30 16:30:48 CEST 2015
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.
More information about the isabelle-dev