It is interesting to look at competing systems and note that every one of them appears to be fully committed to a plain ASCII syntax as the only way of writing a formula. I think it may still be premature to abolish having ASCII even as an alternative syntax.
I wonder whether the appearance of HOL.thy is that important to a typical beginner. Although it sets out the basic logic, it is full of implementation-specific details. I don’t really see how having ∧ in place of & would improve its legibility. Then allowing users to use the & symbol with some other meaning seems quite risky, at least in the short term. Larry Paulson > On 29 Jun 2015, at 23:23, C. Diekmann <diekm...@in.tum.de> wrote: > > 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
