[isabelle-dev] Isabelle2016-RC0: potential changes

[Makarius]

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