src/HOL/Algebra/poly/UnivPoly2.thy
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-02-20 haftmann 2009-02-20 fixed spurious proof failure
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
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 separate class dvd for divisibility predicate
2008-04-07 haftmann 2008-04-07 explicit dummy instantiation for div
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
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-06-13 wenzelm 2007-06-13 tuned proofs: avoid implicit prems;
2007-05-11 wenzelm 2007-05-11 tuned proofs;
2006-11-19 wenzelm 2006-11-19 HOL-Algebra: converted legacy ML scripts;
2006-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-08-02 webertj 2006-08-02 lin_arith_prover splits certain operators (e.g. min, max, abs)
2005-07-01 berghofe 2005-07-01 Removed setsubgoaler hack (thanks to strong_setsum_cong).
2005-05-23 nipkow 2005-05-23 tuned setsum rewrites
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-07-15 nipkow 2004-07-15 Moved to new m<..<n syntax for set intervals.
2004-04-16 wenzelm 2004-04-16 simplified ML code for setsubgoaler;
2003-04-30 ballarin 2003-04-30 Greatly extended CRing. Added Module.