Some symbols like ! and ? are quick to type but I wouldn't call them "graphical" and am not particularly attached to them. In fact, one could then give factorial its standard syntax.
Tobias On 30/06/2015 14:13, Makarius wrote:
On Tue, 30 Jun 2015, C. Diekmann wrote: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.Interesting that you call this "legacy ASCII" syntax. In the manner it is done until today, the ASCII syntax is still the official syntax and the "xsymbols" variant some add-on. Only recently, the system default has changed to have "xsymbols" always enabled by default. Historically, there were good reasons of having the system act in plain ASCII by default, due to a general lack of reliability in rendering Isabelle symbols on various operating systems, terminal emulators, and versions of Emacs. Now that the TTY loop and Proof General are removed, there is nothing to prevent a fresh look at the situation. Here are just the canonical questions (which are never meant rhetoric): (1) Are there remaining uses of plain ASCII syntax in Isabelle output? (2) Are there remaining uses of plain ASCII syntax in Isabelle input? As a start to the collection of material some possible points: Concerning output: * Seemingly modern web frameworks might lack Unicode rendering quality to work with Isabelle symbols relibly. 1-2 years ago there were still problems on Stackoverflow. Do they still exist? In contrast, plain HTML pages should be able to provide the IsabelleText font from the server side. There is no need for the old "HTML" print mode. Concerning input: * Compatibility: huge amounts of existing sources still use ASCII input. There are chances to make a systematic upgrade for formally checked text, but not for unchecked comments. * Convenience: users somethings find it too combersome to type proper Isabelle symbols. I never do that myself, but take the time to type things nicely. It is actually not much time for me, since I implemented the input methods myself and know how they work. Anything further points? Once the collection of observation is complete, we can come up with further migration plans to improve on the historical situation. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
