[isabelle-dev] Deprecating legacy ASCII symbols?

[Larry Paulson]

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 <diekmann at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev