src/HOL/Deriv.thy
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