Re: [isabelle-dev] Preferred syntax for big GCD?

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 \ A. f x >> >> An

Re: [isabelle-dev] Preferred syntax for big GCD?

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 \ A. f x An alternative could be (b) GCD x \ A. f x The form (b) follows the tradition to have binders all-capitalized (SUP, INF, UNION, INTER, THE,

Re: [isabelle-dev] Preferred syntax for big GCD?

I’m sympathetic to this view. On the other hand, GCD is the only one of these uppercase formulations that’s actually in widespread use. Larry > On 10 Mar 2016, at 09:46, Florian Haftmann > wrote: > > Since there is no generally accepted symbolic

Re: [isabelle-dev] Preferred syntax for big GCD?

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 \ A. f x An alternative could be (b) GCD x \ A. f x The form (b) follows the tradition to have binders

[isabelle-dev] Preferred syntax for big GCD?

Hi all, in 66a381d3f88f, the usual syntax for big operators has been added for GCD (and LCM): (a) Gcd x \ A. f x An alternative could be (b) GCD x \ 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