src/HOL/Algebra/Exponent.thy
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-02-21 ago Removed subsumed lemmas
2009-02-20 ago consider changes variable names in theorem le_imp_power_dvd
2008-08-01 ago Generalised polynomial lemmas from cring to ring.
2008-07-18 ago moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-06-10 ago slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2007-10-23 ago went back to >0
2007-10-21 ago Eliminated most of the neq0_conv occurrences. As a result, many
2007-09-27 ago removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
2007-07-24 ago fixed proofs involving dvd;
2006-11-08 ago moved theories Parity, GCD, Binomial to Library;
2006-08-30 ago lin_arith_prover: splitting reverted because of performance loss
2006-08-03 ago Restructured algebra library, added ideals and quotient rings.
2006-08-02 ago lin_arith_prover splits certain operators (e.g. min, max, abs)
2005-07-07 ago linear arithmetic now takes "&" in assumptions apart.
2005-07-01 ago prime is a predicate now.
2005-06-17 ago migrated theory headers to new format
2004-06-09 ago moved some cardinality results into main HOL
2004-05-06 ago tuned document;
2003-03-18 ago moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them