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