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
gcd/lcm/Gcd/Lcm.

* 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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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