src/HOL/Library/Polynomial.thy
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-07-12 haftmann 2010-07-12 avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 dropped mk_left_commute; use interpretation of locale abel_semigroup instead
2010-01-10 berghofe 2010-01-10 Adapted to changes in induct method.
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-16 huffman 2009-06-16 smult_dvd lemmas; polynomial gcd
2009-04-29 haftmann 2009-04-29 farewell to class recpower
2009-04-22 haftmann 2009-04-22 power operation defined generic
2009-04-16 haftmann 2009-04-16 tightended specification of class semiring_div
2009-03-27 haftmann 2009-03-27 normalized imports
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-27 huffman 2009-02-27 make list-style polynomial syntax work when show_sorts is on
2009-02-23 huffman 2009-02-23 add lemmas poly_{div,mod}_minus_{left,right}
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library