src/HOL/Deriv.thy
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl 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
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:21:00 +0100 hoelzl 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
Tue, 26 Mar 2013 12:20:58 +0100 hoelzl move SEQ.thy and Lim.thy to Limits.thy
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move connected to HOL image; used to show intermediate value theorem
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl clean up lemma_nest_unique and renamed to nested_sequence_unique
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
Tue, 04 Dec 2012 18:00:37 +0100 hoelzl prove tendsto_power_div_exp_0
Tue, 04 Dec 2012 18:00:31 +0100 hoelzl 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
Mon, 03 Dec 2012 18:19:12 +0100 hoelzl use filterlim in Lim and SEQ; tuned proofs
Mon, 03 Dec 2012 18:19:11 +0100 hoelzl conversion rules for at, at_left and at_right; applied to l'Hopital's rules.
Mon, 03 Dec 2012 18:19:09 +0100 hoelzl weakened assumptions for lhopital_right_0
Mon, 03 Dec 2012 18:19:08 +0100 hoelzl tuned proof
Mon, 03 Dec 2012 18:19:07 +0100 hoelzl add L'Hôpital's rule
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Fri, 09 Dec 2011 11:31:13 +0100 noschinl more systematic lemma name
Sun, 20 Nov 2011 17:44:41 +0100 wenzelm 'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Tue, 13 Sep 2011 17:07:33 -0700 huffman tuned proofs
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Fri, 19 Aug 2011 18:06:27 -0700 huffman remove redundant lemma lemma_DERIV_subst in favor of DERIV_cong
Fri, 19 Aug 2011 15:54:43 -0700 huffman Lim.thy: legacy theorems
Tue, 16 Aug 2011 09:31:23 -0700 huffman add simp rules for isCont
Mon, 15 Aug 2011 09:08:17 -0700 huffman simplify some proofs
Mon, 08 Aug 2011 16:57:37 -0700 huffman remove duplicate lemmas
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Tue, 21 Dec 2010 15:00:59 +0100 hoelzl use DERIV_intros
Tue, 20 Jul 2010 06:35:29 +0200 haftmann robustified metis proof
Mon, 19 Jul 2010 20:19:03 +0200 haftmann diff_eq_diff_less_eq' replaces diff_eq_diff_less_eq
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Sun, 09 May 2010 17:47:43 -0700 huffman avoid using real-specific versions of generic lemmas
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Sun, 15 Nov 2009 00:34:21 +0100 wenzelm simplified bulky metis proofs;
Fri, 13 Nov 2009 15:38:45 +0100 wenzelm more "anti_sym" -> "antisym" (cf. a4179bf442d1);
Fri, 13 Nov 2009 11:33:33 +0000 paulson A number of theorems contributed by Jeremy Avigad
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Thu, 02 Jul 2009 15:37:22 +0200 wenzelm fixed document (DERIV_intros);
Tue, 30 Jun 2009 18:16:22 +0200 hoelzl Added DERIV_intros
Tue, 02 Jun 2009 23:31:03 -0700 huffman generalize type of constant lim
Fri, 29 May 2009 09:22:56 -0700 huffman generalize constants from Lim.thy to class metric_space
Thu, 28 May 2009 22:57:17 -0700 huffman generalize constants in SEQ.thy to class metric_space
Tue, 28 Apr 2009 15:50:30 +0200 haftmann stripped class recpower further
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Wed, 18 Feb 2009 20:14:45 -0800 huffman move Polynomial.thy to Library
Wed, 18 Feb 2009 19:32:26 -0800 huffman split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
Wed, 18 Feb 2009 17:02:00 -0800 huffman finish converting Deriv.thy to new polynomial library
Wed, 18 Feb 2009 09:07:36 -0800 huffman more subsection headings
Thu, 05 Feb 2009 11:34:42 +0100 hoelzl Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Tue, 13 Jan 2009 08:19:14 -0800 huffman declare smult rules [simp]
less more (0) -60 tip