Re: [isabelle] Code setup for Fraction_Field

I just looked at all of this again and found the situation to be much more painful than I had remembered. In the long run, we definitely want to replace the definitions of the gcd for natural numbers and integers with the gcd_eucl, and then add the current definitions as alternative definitions and code equations.

I just slighly modified his version to move most of theorems presented in
the euclidean_ring_gcd class to the euclidean_ring one.
I also concluded that that is pretty much the only viable option (other than doing the change I mentioned above, which is probably also what Andreas meant initially).

I guess Florian had planned to do this anyway in the course of his refactoring of algebraic type classes, but I don't know what his current status is on that.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.