[isabelle-dev] Preferred syntax for big GCD?

[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