[isabelle-dev] Isabelle2016-RC0: potential changes

Makarius makarius at sketis.net
Thu Jan 14 15:36:36 CET 2016

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.)


More information about the isabelle-dev mailing list