[isabelle-dev] Preferred syntax for big GCD?

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160310/c2a42569/attachment.bin>