On Tue, 12 Jan 2016, Manuel Eberl wrote:
So why should the small proof below be not integrated for the 2016
release?
This is probably a question for Florian. I introduced Euclidean rings to
allow a more systematic derivation of (constructive) GCDs about two years ago
or so.
As for the release, perhaps Florian can comment on whether anything
speaks against moving this instance into the Polynomial theory.
I can't say anything specific about these parts of the library, but
generally I would be glad to see this sorted out for this release. There
is approximately all of this week left to add such small things -- and to
get AFP into proper shape as well.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
