src/HOL/Library/Poly_Deriv.thy
2015-08-06 haftmann 2015-08-06 slight cleanup of lemmas
2015-07-08 haftmann 2015-07-08 avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-07 haftmann 2014-09-07 explicit theory with additional, less commonly used list operations
2014-04-03 paulson 2014-04-03 Cleaned up some messy proofs
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-03-19 paulson 2014-03-19 Some rationalisation of basic lemmas
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-08-19 huffman 2011-08-19 remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2009-06-30 hoelzl 2009-06-30 use DERIV_intros
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-18 huffman 2009-02-18 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy