[isabelle-dev] Preferred syntax for big GCD?
florian.haftmann at informatik.tu-muenchen.de
Thu Mar 10 10:46:00 CET 2016
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?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev