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