[isabelle-dev] Isabelle2016-RC0: potential changes
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