src/HOL/Deriv.thy
2012-03-25 ago merged fork with new numeral representation (see NEWS)
2011-12-09 ago more systematic lemma name
2011-11-20 ago 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-10-28 ago tuned Named_Thms: proper binding;
2011-09-22 ago discontinued legacy theorem names from RealDef.thy
2011-09-13 ago tuned proofs
2011-09-12 ago new fastforce replacing fastsimp - less confusing name
2011-08-28 ago discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-19 ago remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19 ago Lim.thy: legacy theorems
2011-08-16 ago add simp rules for isCont
2011-08-15 ago simplify some proofs
2011-08-08 ago remove duplicate lemmas
2011-01-14 ago eliminated global prems;
2010-12-21 ago use DERIV_intros
2010-07-20 ago robustified metis proof
2010-07-19 ago diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
2010-07-19 ago diff_minus subsumes diff_def
2010-05-09 ago avoid using real-specific versions of generic lemmas
2010-02-18 ago get rid of many duplicate simp rule warnings
2010-01-16 ago dropped some old primrecs and some constdefs
2009-11-15 ago simplified bulky metis proofs;
2009-11-13 ago more "anti_sym" -> "antisym" (cf. a4179bf442d1);
2009-11-13 ago A number of theorems contributed by Jeremy Avigad
2009-07-02 ago renamed NamedThmsFun to Named_Thms;
2009-07-02 ago fixed document (DERIV_intros);
2009-06-30 ago Added DERIV_intros
2009-06-02 ago generalize type of constant lim
2009-05-29 ago generalize constants from Lim.thy to class metric_space
2009-05-28 ago generalize constants in SEQ.thy to class metric_space
2009-04-28 ago stripped class recpower further
2009-03-04 ago declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-02-18 ago move Polynomial.thy to Library
2009-02-18 ago split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-18 ago finish converting Deriv.thy to new polynomial library
2009-02-18 ago more subsection headings
2009-02-05 ago Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-01-28 ago Replaced group_ and ring_simps by algebra_simps;
2009-01-13 ago declare smult rules [simp]
2009-01-13 ago convert Deriv.thy to use new Polynomial library (incomplete)
2008-12-24 ago more proofs about differentiable
2008-12-24 ago move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-03 ago made repository layout more coherent with logical distribution structure; stripped some $Id$s