src/HOL/Algebra/abstract/Ring2.thy
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-03-21 wenzelm 2010-03-21 slightly more uniform definitions -- eliminated old-style meta-equality;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-24 haftmann 2010-02-24 tuned comment
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-08-29 wenzelm 2009-08-29 eliminated hard tabs;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-01-28 nipkow 2009-01-28 merged
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-28 haftmann 2009-01-28 explicit check for exactly one type variable in class specification elements
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-07-11 haftmann 2008-07-11 class instead of axclass
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-03-19 wenzelm 2008-03-19 more antiquotations;
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.