Dear all, 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. Cheers, Jose 2016-02-28 21:29 GMT+01:00 Manuel Eberl <ebe...@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 > 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 <ebe...@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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
