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