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