src/HOL/MacLaurin.thy
2017-03-16 paulson 2017-03-16 Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-07-31 wenzelm 2016-07-31 simplified theory structure;
2016-07-31 wenzelm 2016-07-31 misc tuning and modernization;
2016-07-02 haftmann 2016-07-02 more theorems
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "abs";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-04-11 paulson 2015-04-11 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-19 haftmann 2014-10-19 prefer generic elimination rules for even/odd over specialized unfold rules for nat
2014-09-21 haftmann 2014-09-21 explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-03-21 paulson 2014-03-21 a few new lemmas and generalisations of old ones
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-19 huffman 2011-08-19 move sin_coeff and cos_coeff lemmas to Transcendental.thy; simplify some proofs
2011-08-19 huffman 2011-08-19 Transcendental.thy: remove several unused lemmas and simplify some proofs
2011-08-19 huffman 2011-08-19 fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
2010-12-15 hoelzl 2010-12-15 beautify MacLaurin proofs; make better use of DERIV_intros
2010-12-15 bulwahn 2010-12-15 adding an Isar version of the MacLaurin theorem from some students' work in 2005
2010-05-17 huffman 2010-05-17 remove some unnamed simp rules from Transcendental.thy; move the needed ones to MacLaurin.thy where they are used
2009-07-17 avigad 2009-07-17 Changed fact_Suc_nat back to fact_Suc
2009-07-10 avigad 2009-07-10 Repaired uses of factorial.
2009-06-30 hoelzl 2009-06-30 remove DERIV_tac and deriv_tac, neither is used in Isabelle/HOL or the AFP
2009-06-30 hoelzl 2009-06-30 use DERIV_intros
2009-05-14 nipkow 2009-05-14 Cleaned up Parity a little
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2009-02-24 huffman 2009-02-24 make more proofs work whether or not One_nat_def is a simp rule
2009-02-06 chaieb 2009-02-06 fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
2009-02-05 hoelzl 2009-02-05 Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
2008-12-28 huffman 2008-12-28 clean up proofs of lemma Maclaurin
2008-12-24 huffman 2008-12-24 use less_iff_Suc_add instead of less_add_one
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s