Then let's got for capitalization. See now 92680537201f.
FlorianAm 09.04.2016 um 22:05 schrieb Makarius: > On Thu, 10 Mar 2016, Florian Haftmann wrote: > >> in 66a381d3f88f, the usual syntax for big operators has been added for >> GCD (and LCM): >> >> (a) Gcd x \<in> A. f x >> >> An alternative could be >> >> (b) GCD x \<in> A. f x >> >> The form (b) follows the tradition to have binders all-capitalized (SUP, >> INF, UNION, INTER, THE, LEAST, SUM, PROD). >> >> On the other hand nearly all those binders have pretty symbolic syntax, >> such that the all-capitalized variants rarely show up in theory text. >> Since there is no generally accepted symbolic syntax for gcd, it might >> be better to let the (slightly more readable) form (a) stand. > > This thread is still open in current Isabelle/ef8d840f39fb. > > As far as I can tell, the canonical form for binder-like syntax in ASCII > is UPPERCASE. > > I've recently made several rounds in replacing a lot of ASCII notation > by Isabelle symbols, and thus can confirm that the situation of > remaining ASCII usually follows that convention. > > > Makarius > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
