[isabelle-dev] buildall inconsistency
jose.divasonm at unirioja.es
Tue Mar 1 12:43:34 CET 2016
Thanks Manuel for your changes about euclidean rings!
Jesús Aransay and I are now introducing a few changes in the Echelon_Form
development. In addition, we are also polishing the code. We hope to finish
it in the following days.
2016-02-28 21:29 GMT+01:00 Manuel Eberl <eberlm at in.tum.de>:
> 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
> On 28/02/16 15:45, Lawrence Paulson wrote:
>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev