[isabelle-dev] Deprecating legacy ASCII symbols?

[C. Diekmann]

Dear list,

the following mail may contain a stupid idea.

In HOL.thy, the conjunction (conj) is first introduced with the "&"
symbol. Later, the notation "∧" is introduced. In order to clean up
this difficult-to-understand theory, would it be possible to directly
introduce conjunction with the "∧" symbol? I see three advantages:

1) It simplifies the axiomatizations (a very critical part).
2) It may help in getting started with Isabelle since no confusing "&"
symbol would appear anywhere. Currently, if a ctrl-click on a lemma
sends me to HOL.thy, things look pretty scary.
3) It would free up the symbol "&" for custom theories.

This could also be done for %, -->, ==, ~, and many more.

I guess this would break a lot, that's why I'm posting on dev.

Best,
  Cornelius