[isabelle-dev] Isabelle2016-RC0: potential changes
makarius at sketis.net
Tue Jan 12 14:08:35 CET 2016
On Tue, 12 Jan 2016, Manuel Eberl wrote:
>> So why should the small proof below be not integrated for the 2016
> 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.
More information about the isabelle-dev