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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
