src/HOL/Algebra/ringsimp.ML
2007-04-11 haftmann 2007-04-11 canonical merge operations
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic; tuned;
2006-09-15 wenzelm 2006-09-15 tuned;
2006-08-08 haftmann 2006-08-08 abandoned equal_list in favor for eq_list
2006-07-19 ballarin 2006-07-19 Reimplemented algebra method; now controlled by attribute.
2006-07-14 ballarin 2006-07-14 Term.term_lpo takes order on terms rather than strings as argument.
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-06-25 nipkow 2005-06-25 Changes due to new abel_cancel.ML
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-06-17 paulson 2004-06-17 removal of magmas and semigroups
2004-02-19 ballarin 2004-02-19 New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.
2003-04-30 ballarin 2003-04-30 Greatly extended CRing. Added Module.
2003-03-14 ballarin 2003-03-14 Bugs fixed and operators finprod and finsum.
2003-03-10 ballarin 2003-03-10 First distributed version of Group and Ring theory.