[isabelle-dev] Deprecating legacy ASCII symbols?
diekmann at in.tum.de
Tue Jun 30 00:23:15 CEST 2015
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.
More information about the isabelle-dev