src/HOL/Transcendental.thy
2010-08-23 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
2010-07-19 haftmann diff_minus subsumes diff_def
2010-05-17 huffman remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2010-05-17 huffman remove simp attribute from square_eq_1_iff
2010-05-12 huffman fix some linarith_split_limit warnings
2010-05-11 huffman move some theorems from RealPow.thy to Transcendental.thy
2010-05-10 huffman avoid using real-specific versions of generic lemmas
2010-05-09 huffman remove a couple of redundant lemmas; simplify some proofs
2010-02-18 huffman get rid of many duplicate simp rule warnings
2010-02-18 huffman fix looping call to simplifier
2010-02-08 haftmann more precise proofs
2010-02-05 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann new theory Algebras.thy for generic algebraic structures
2009-11-13 paulson A little rationalisation
2009-11-10 wenzelm tuned proofs;
2009-10-17 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
2009-07-17 avigad Changed fact_Suc_nat back to fact_Suc
2009-07-10 avigad Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
2009-06-30 hoelzl use DERIV_intros
2009-06-30 hoelzl Added DERIV_intros
2009-06-24 nipkow corrected and unified thm names
2009-05-29 huffman generalize constants from Lim.thy to class metric_space
2009-05-27 huffman add constants sin_coeff, cos_coeff
2009-05-14 nipkow Cleaned up Parity a little
2009-04-28 haftmann stripped class recpower further
2009-03-05 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-24 huffman make more proofs work whether or not One_nat_def is a simp rule
2009-02-05 hoelzl Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2009-01-30 chaieb Added real related theorems from Fact.thy
2009-01-28 nipkow Replaced group_ and ring_simps by algebra_simps;
2008-12-24 huffman clean up lemmas about ln
2008-12-24 huffman clean up lemmas about exp
2008-12-24 huffman rearranged subsections; cleaned up some proofs
2008-12-24 huffman move theorems about limits from Transcendental.thy to Deriv.thy
2008-12-24 huffman cleaned up some proofs; removed redundant simp rules
2008-12-23 huffman move sin and cos to their own subsection
2008-12-23 huffman clean up some proofs; remove unused lemmas
2008-12-03 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip