[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

Dear all,

> 
> I have already some post-release patches in the pipeline which would add
> this instance anyway.  So, there is no demand for action here at the moment.
> 
> 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.

And since you want to include the patch anyway, why not include at least the instance now?

Cheers,
René