THE, LEAST, GCD. Tobias
On 10/03/2016 10:46, Florian Haftmann wrote:
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
_______________________________________________
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
