src/HOL/Algebra/ringsimp.ML
2012-04-23 wenzelm 2012-04-23 more standard method setup;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2010-03-21 wenzelm 2010-03-21 standard headers;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-11-08 wenzelm 2009-11-08 tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
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.