[isabelle-dev] buildall inconsistency
lp15 at cam.ac.uk
Sun Feb 28 15:45:11 CET 2016
Looks like valuable work even if it caused some disruption.
> 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.
More information about the isabelle-dev