src/HOL/MacLaurin.thy
Sat, 29 Dec 2018 15:43:53 +0100 nipkow capitalize proper names in lemma names
Thu, 20 Sep 2018 18:20:02 +0100 paulson removal of more redundancies, and fixes
Thu, 20 Sep 2018 14:17:58 +0100 paulson elimination of near duplication involving Rolle's theorem and the MVT
Sat, 21 Jul 2018 23:25:22 +0200 paulson fixing a theorem statement, etc.
Sat, 21 Jul 2018 13:30:43 +0200 paulson de-applying and removing junk
Sat, 12 May 2018 22:20:46 +0200 haftmann removed some non-essential rules
Sun, 26 Nov 2017 21:08:32 +0100 wenzelm more symbols;
Thu, 16 Mar 2017 13:55:29 +0000 paulson Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Sun, 31 Jul 2016 18:05:20 +0200 wenzelm simplified theory structure;
Sun, 31 Jul 2016 17:25:38 +0200 wenzelm misc tuning and modernization;
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 28 Dec 2015 19:23:15 +0100 wenzelm more symbols;
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Wed, 30 Sep 2015 16:36:42 +0100 paulson real_of_nat_Suc is now a simprule
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Sat, 11 Apr 2015 11:56:40 +0100 paulson Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Sun, 19 Oct 2014 18:05:26 +0200 haftmann prefer generic elimination rules for even/odd over specialized unfold rules for nat
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Wed, 11 Jun 2014 14:24:23 +1000 Thomas Sewell Hypsubst preserves equality hypotheses
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Fri, 21 Mar 2014 15:36:00 +0000 paulson a few new lemmas and generalisations of old ones
Tue, 18 Mar 2014 15:53:48 +0100 hoelzl cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
Mon, 17 Mar 2014 19:12:52 +0100 hoelzl unify syntax for has_derivative and differentiable
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
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