src/HOL/Algebra/abstract/Ring.thy
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-23 nipkow 2005-05-23 tuned setsum rewrites
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-07-08 wenzelm 2004-07-08 tuned;
2004-05-11 obua 2004-05-11 changes made due to new Ring_and_Field theory
2004-03-05 paulson 2004-03-05 tweaked for times_ac1
2003-01-23 ballarin 2003-01-23 Fixed term order for normal form in rings.
2002-11-28 ballarin 2002-11-28 HOL-Algebra partially ported to Isar.
2001-10-15 wenzelm 2001-10-15 ring includes plus_ac0;
2001-02-10 ballarin 2001-02-10 Changes to HOL/Algebra: - Axclasses consolidated (axiom one_not_zero). - Now uses summation operator setsum; SUM has been removed. - Priority of infix assoc changed to 50, in accordance to dvd.
2000-11-10 wenzelm 2000-11-10 use inverse, divide from basic HOL;
2000-07-19 paulson 2000-07-19 renamed // to / (which is what we want anyway) to avoid clash with the new use of // for quotienting
1999-11-05 paulson 1999-11-05 Algebra and Polynomial theories, by Clemens Ballarin