[isabelle-dev] Isabelle2016-RC0: potential changes

[Makarius]

On Thu, 14 Jan 2016, Florian Haftmann wrote:

>>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>>> thus very hardly different from syntactic classes, so there is no loss
>>> of generality here.
>>
>> I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have
>> the three essential lemmas:
>>
>> gcd_dvd1, gcd_dvd2, and gcd_greatest.
>
> indeed, but these are exactly the assumptions of the type class.
>
>> And since you want to include the patch anyway, why not include at least the instance now?
>
> It sits on top of a couple of other patches definitely not suitable for
> inclusion by now.

Does it mean this thread is closed concerning Isabelle2016?

We can probably afford a few more days to stabilize the conclusion of the 
various "potential changes".  (I can't contribute anything myself, because 
I don't know these parts of the library.)


 	Makarius