src/HOL/Transcendental.thy
Mon, 14 Mar 2011 14:37:35 +0100 hoelzl generalize infinite sums
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
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
Mon, 17 May 2010 08:45:46 -0700 huffman remove simp attribute from square_eq_1_iff
Tue, 11 May 2010 19:38:16 -0700 huffman fix some linarith_split_limit warnings
Tue, 11 May 2010 06:30:48 -0700 huffman move some theorems from RealPow.thy to Transcendental.thy
Sun, 09 May 2010 17:47:43 -0700 huffman avoid using real-specific versions of generic lemmas
Sun, 09 May 2010 14:21:44 -0700 huffman remove a couple of redundant lemmas; simplify some proofs
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Thu, 18 Feb 2010 08:08:51 -0800 huffman fix looping call to simplifier
Mon, 08 Feb 2010 14:06:58 +0100 haftmann more precise proofs
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 13 Nov 2009 17:15:12 +0000 paulson A little rationalisation
Tue, 10 Nov 2009 14:38:06 +0100 wenzelm tuned proofs;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Fri, 17 Jul 2009 13:12:18 -0400 avigad Changed fact_Suc_nat back to fact_Suc
Fri, 10 Jul 2009 10:45:30 -0400 avigad Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
Tue, 30 Jun 2009 18:21:55 +0200 hoelzl use DERIV_intros
Tue, 30 Jun 2009 18:16:22 +0200 hoelzl Added DERIV_intros
Wed, 24 Jun 2009 09:41:14 +0200 nipkow corrected and unified thm names
Fri, 29 May 2009 09:22:56 -0700 huffman generalize constants from Lim.thy to class metric_space
Wed, 27 May 2009 16:39:22 -0700 huffman add constants sin_coeff, cos_coeff
Thu, 14 May 2009 15:39:15 +0200 nipkow Cleaned up Parity a little
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
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
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
Fri, 30 Jan 2009 12:48:57 +0000 chaieb Added real related theorems from Fact.thy
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Wed, 24 Dec 2008 13:29:49 -0800 huffman clean up lemmas about ln
Wed, 24 Dec 2008 13:16:26 -0800 huffman clean up lemmas about exp
Wed, 24 Dec 2008 08:40:16 -0800 huffman rearranged subsections; cleaned up some proofs
Wed, 24 Dec 2008 08:16:45 -0800 huffman move theorems about limits from Transcendental.thy to Deriv.thy
Wed, 24 Dec 2008 08:06:27 -0800 huffman cleaned up some proofs; removed redundant simp rules
Tue, 23 Dec 2008 15:02:30 -0800 huffman move sin and cos to their own subsection
Tue, 23 Dec 2008 14:31:47 -0800 huffman clean up some proofs; remove unused lemmas
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