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 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 just slighly modified his version to move most of theorems presented in
the euclidean_ring_gcd class to the euclidean_ring one.
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