[isabelle-dev] buildall inconsistency

[Manuel Eberl]

I just successfully built the entire distribution and the entire AFP. 
(Isabelle a3c7bd201da7 / AFP 6d199a5)

I also removed the rogue "Euclidean Ring" definition and orphaned 
instances in Echelon_Form, but I think that Echelon_Form, Hermite, 
Algebraic_Numbers and the related entries are in dire need of a major 
cleanup. Echelon_Form/Rings2 in particular contains a lot of interesting 
material.


Cheers,

Manuel


On 28/02/16 15:45, Lawrence Paulson wrote:
> 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.
>>
>