[isabelle-dev] Preferred syntax for big GCD?

[Florian Haftmann]

Then let's got for capitalization.  See now 92680537201f.

	Florian

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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160421/1916d6da/attachment.sig>