Hi Rene, >> 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.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
