Re: [isabelle] Code setup for Fraction_Field

This discussion is leaving the scope of isabelle-users since we are
talking about ongoing developments in the Isabelle repository,
nevertheless here a short preview:

* The next Isabelle release will (in Complex-Main) contain type classes
for generic gcd, lcm, Gcd, Lcm with the most fundamental instances
(hence no euquivalence problems).

* Before we can continue to move the euclidean algorithm itself to
Complex-Main, the existing theories must be cleaned-up by removing
duplicates, generalizing what can be generalized etc concerning

* After that, the euclidean algorithm can be absorbed into Complex-Main.

I have this on my agenda, but not prioritized.  Any help concerning the
GCD cleanup is appreciated.

Detaisl could be discussed on isabelle-dev.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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