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é _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
