[isabelle-dev] Isabelle2016-RC0: potential changes
Rene.Thiemann at uibk.ac.at
Thu Jan 14 11:31:23 CET 2016
> 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?
More information about the isabelle-dev