[isabelle-dev] Preferred syntax for big GCD?
florian.haftmann at informatik.tu-muenchen.de
Thu Apr 21 08:42:43 CEST 2016
Then let's got for capitalization. See now 92680537201f.
Am 09.04.2016 um 22:05 schrieb Makarius:
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev