src/HOL/Algebra/abstract/Ring2.thy
2008-01-02 haftmann 2008-01-02 splitted class uminus from class minus
2007-10-12 haftmann 2007-10-12 class div inherits from class times
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-04-26 wenzelm 2007-04-26 eliminated unnamed infixes, tuned syntax;
2007-03-02 haftmann 2007-03-02 prefix of class interpretation not mandatory any longer
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;
2006-11-18 haftmann 2006-11-18 dvd_def now with object equality
2006-08-03 ballarin 2006-08-03 Restructured algebra library, added ideals and quotient rings.