src/HOL/Deriv.thy
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]
Tue, 13 Jan 2009 06:57:08 -0800 huffman convert Deriv.thy to use new Polynomial library (incomplete)
Wed, 24 Dec 2008 11:17:37 -0800 huffman more proofs about differentiable
Wed, 24 Dec 2008 08:16:45 -0800 huffman move theorems about limits from Transcendental.thy to Deriv.thy
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip