[isabelle-dev] buildall inconsistency

[Lawrence Paulson]

Looks like valuable work even if it caused some disruption.
Larry

> On 28 Feb 2016, at 13:32, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> Yes, this has something to do with my ongoing changes to Euclidean Rings and related stuff. Everything in the distribution already works again and, as for the AFP, I'm on it.
> 
> I've removed all of the redundant facts in Euclidean_Algorithm and moved all the facts that are not specific to Euclidean Rings to semiring_gcd and ring_gcd. I also took care of the appropriate subclass instances and fixed code generation for Gcd/Lcm.
> 
> Most importantly, I also adapted all the AFP entries that use the polynomial GCD to work with the GCD from Euclidean_Algorithm instead of their own instances.
> 
> We should be able to move Euclidean_Algorithm out of Number_Theory and into the main HOL soon.
>