src/HOL/Library/Commutative_Ring.thy
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-10 haftmann 2007-12-10 switched import from Main to List
2007-06-23 nipkow 2007-06-23 tuned and renamed group_eq_simps and ring_eq_simps
2007-04-20 haftmann 2007-04-20 switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
2007-04-13 wenzelm 2007-04-13 tuned document (headers, sections, spacing);
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-09-22 wenzelm 2006-09-22 tuned proofs;
2006-09-19 wenzelm 2006-09-19 tuned proofs;
2006-05-27 wenzelm 2006-05-27 tuned;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-09-20 wenzelm 2005-09-20 added Commutative_Ring (from Main HOL);