src/HOL/Deriv.thy
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-26 hoelzl 2013-03-26 move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
2013-03-26 hoelzl 2013-03-26 move SEQ.thy and Lim.thy to Limits.thy
2013-03-22 hoelzl 2013-03-22 move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
2013-03-22 hoelzl 2013-03-22 move connected to HOL image; used to show intermediate value theorem
2013-03-22 hoelzl 2013-03-22 move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
2013-03-22 hoelzl 2013-03-22 clean up lemma_nest_unique and renamed to nested_sequence_unique
2013-03-22 hoelzl 2013-03-22 simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
2012-12-04 hoelzl 2012-12-04 prove tendsto_power_div_exp_0 * * * missing rename
2012-12-04 hoelzl 2012-12-04 add filterlim rules for eventually monotone bijective functions; mirror rules for at_top, at_bot; apply them to prove convergence of arctan at infinity and tan at pi/2
2012-12-03 hoelzl 2012-12-03 use filterlim in Lim and SEQ; tuned proofs
2012-12-03 hoelzl 2012-12-03 conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
2012-12-03 hoelzl 2012-12-03 weakened assumptions for lhopital_right_0
2012-12-03 hoelzl 2012-12-03 tuned proof
2012-12-03 hoelzl 2012-12-03 add L'Hôpital's rule
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-12-09 noschinl 2011-12-09 more systematic lemma name
2011-11-20 wenzelm 2011-11-20 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-22 huffman 2011-09-22 discontinued legacy theorem names from RealDef.thy
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-19 huffman 2011-08-19 remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
2011-08-19 huffman 2011-08-19 Lim.thy: legacy theorems
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-15 huffman 2011-08-15 simplify some proofs
2011-08-08 huffman 2011-08-08 remove duplicate lemmas
2011-01-14 wenzelm 2011-01-14 eliminated global prems; tuned proofs;
2010-12-21 hoelzl 2010-12-21 use DERIV_intros
2010-07-20 haftmann 2010-07-20 robustified metis proof
2010-07-19 haftmann 2010-07-19 diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-05-09 huffman 2010-05-09 avoid using real-specific versions of generic lemmas
2010-02-18 huffman 2010-02-18 get rid of many duplicate simp rule warnings
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2009-11-15 wenzelm 2009-11-15 simplified bulky metis proofs;
2009-11-13 wenzelm 2009-11-13 more "anti_sym" -> "antisym" (cf. a4179bf442d1);
2009-11-13 paulson 2009-11-13 A number of theorems contributed by Jeremy Avigad
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-07-02 wenzelm 2009-07-02 fixed document (DERIV_intros); minor tuning;
2009-06-30 hoelzl 2009-06-30 Added DERIV_intros
2009-06-02 huffman 2009-06-02 generalize type of constant lim
2009-05-29 huffman 2009-05-29 generalize constants from Lim.thy to class metric_space
2009-05-28 huffman 2009-05-28 generalize constants in SEQ.thy to class metric_space
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-18 huffman 2009-02-18 move Polynomial.thy to Library
2009-02-18 huffman 2009-02-18 split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
2009-02-18 huffman 2009-02-18 finish converting Deriv.thy to new polynomial library
2009-02-18 huffman 2009-02-18 more subsection headings
2009-02-05 hoelzl 2009-02-05 Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-01-28 nipkow 2009-01-28 Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
2009-01-13 huffman 2009-01-13 declare smult rules [simp]
2009-01-13 huffman 2009-01-13 convert Deriv.thy to use new Polynomial library (incomplete)
2008-12-24 huffman 2008-12-24 more proofs about differentiable
2008-12-24 huffman 2008-12-24 move theorems about limits from Transcendental.thy to Deriv.thy