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?
We can probably afford a few more days to stabilize the conclusion of the
various "potential changes". (I can't contribute anything myself, because
I don't know these parts of the library.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
