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