[isabelle-dev] Isabelle2016-RC0: potential changes

Thiemann, Rene Rene.Thiemann at uibk.ac.at
Thu Jan 14 11:31:23 CET 2016

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?


More information about the isabelle-dev mailing list