src/HOL/MacLaurin.thy
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 19 Aug 2011 18:42:41 -0700 huffman move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
Fri, 19 Aug 2011 10:46:54 -0700 huffman Transcendental.thy: remove several unused lemmas and simplify some proofs
Fri, 19 Aug 2011 08:39:43 -0700 huffman fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
Wed, 15 Dec 2010 15:13:52 +0100 hoelzl beautify MacLaurin proofs; make better use of DERIV_intros
Wed, 15 Dec 2010 08:34:01 +0100 bulwahn adding an Isar version of the MacLaurin theorem from some students' work in 2005
Mon, 17 May 2010 15:58:32 -0700 huffman remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
Fri, 17 Jul 2009 13:12:18 -0400 avigad Changed fact_Suc_nat back to fact_Suc
Fri, 10 Jul 2009 12:55:06 -0400 avigad Repaired uses of factorial.
Tue, 30 Jun 2009 18:24:00 +0200 hoelzl remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP
Tue, 30 Jun 2009 18:21:55 +0200 hoelzl use DERIV_intros
Thu, 14 May 2009 15:39:15 +0200 nipkow Cleaned up Parity a little
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
Fri, 06 Feb 2009 00:10:58 +0000 chaieb fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
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
Sun, 28 Dec 2008 14:40:43 -0800 huffman clean up proofs of lemma Maclaurin
Wed, 24 Dec 2008 09:26:18 -0800 huffman use less_iff_Suc_add instead of less_add_one
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