[isabelle-dev] Preferred syntax for big GCD?

[Florian Haftmann]

Hi all,

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.

I have no strong opinion on this.  Any suggestions?

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160310/57ab71ba/attachment.asc>