> Am 14.01.2016 um 15:36 schrieb Makarius <makar...@sketis.net>: > > 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?
If Florian has a post-release patch available and wants to insert exactly that patch, then that’s fine for me. Then Isabelle users (including myself) can just load the proposed instance declaration from the AFP to uniformly access the gcd-properties via the semiring-class(-axioms) in Isabelle 2016. Cheers, René _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
