src/HOL/Deriv.thy
Mon, 17 Oct 2016 17:33:07 +0200 nipkow setprod -> prod
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Wed, 28 Sep 2016 17:01:01 +0100 paulson new material connected with HOL Light measure theory, plus more rationalisation
Mon, 19 Sep 2016 20:06:21 +0200 fleury left_distrib ~> distrib_right, right_distrib ~> distrib_left
Sun, 18 Sep 2016 20:33:48 +0200 wenzelm tuned proofs;
Thu, 18 Aug 2016 18:11:45 +0200 hoelzl remove spurious find_theorems
Wed, 17 Aug 2016 16:16:38 +0200 eberlm Tuned L'Hospital
Wed, 10 Aug 2016 09:33:54 +0200 nipkow "split add" -> "split"
Mon, 08 Aug 2016 14:13:14 +0200 hoelzl rename HOL-Multivariate_Analysis to HOL-Analysis.
Thu, 28 Jul 2016 20:39:46 +0200 wenzelm misc tuning and modernization;
Wed, 13 Jul 2016 17:14:17 +0100 paulson lots of new theorems about differentiable_on, retracts, ANRs, etc.
Tue, 14 Jun 2016 13:14:11 +0200 eberlm Integration by substitution
Thu, 09 Jun 2016 16:04:20 +0200 immler approximation, derivative, and continuity of floor and ceiling
Fri, 27 May 2016 20:23:55 +0200 wenzelm tuned proofs, to allow unfold_abs_def;
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Tue, 10 May 2016 15:48:37 +0200 immler some slight generalizations
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Wed, 24 Feb 2016 16:00:57 +0000 paulson Merge
Wed, 24 Feb 2016 15:51:01 +0000 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 30 Dec 2015 14:05:51 +0100 wenzelm more symbols;
Wed, 30 Dec 2015 11:21:54 +0100 wenzelm more symbols;
Wed, 09 Dec 2015 17:35:22 +0000 paulson sorted out eventually_mono
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.
Mon, 02 Nov 2015 16:17:09 +0100 eberlm Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Tue, 05 May 2015 18:45:10 +0200 immler moved basic lemmas about has_vector_derivative
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Tue, 31 Mar 2015 15:00:03 +0100 paulson New material and binomial fix
Fri, 06 Mar 2015 12:48:03 +0000 paulson A few new lemmas and a bit of tidying up
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Mon, 20 Oct 2014 18:33:14 +0200 hoelzl add tendsto_const and tendsto_ident_at as simp and intro rules
Sat, 16 Aug 2014 14:42:35 +0200 wenzelm updated to named_theorems;
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Wed, 09 Apr 2014 09:37:48 +0200 hoelzl field_simps: better support for negation and division, and power
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Thu, 03 Apr 2014 23:51:52 +0100 paulson removing simprule status for divide_minus_left and divide_minus_right
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Wed, 26 Mar 2014 14:00:37 +0000 paulson Some useful lemmas
Mon, 24 Mar 2014 14:22:29 +0000 paulson rearranging some deriv theorems
Wed, 19 Mar 2014 21:59:31 +0100 wenzelm tuned proofs;
Wed, 19 Mar 2014 17:06:02 +0000 paulson Some rationalisation of basic lemmas
Mon, 17 Mar 2014 19:50:59 +0100 hoelzl update syntax of has_*derivative to infix 50; fixed proofs
Mon, 17 Mar 2014 19:12:52 +0100 hoelzl unify syntax for has_derivative and differentiable
Fri, 07 Mar 2014 15:52:56 +0000 paulson Some new proofs. Tidying up, esp to remove "apply rule".
Fri, 07 Mar 2014 12:35:06 +0000 paulson a few new lemmas
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:21:00 +0100 hoelzl move theorems about compactness of real closed intervals, the intermediate value theorem, and lemmas about continuity of bijective functions from Deriv.thy to Limits.thy
Tue, 26 Mar 2013 12:20:58 +0100 hoelzl move SEQ.thy and Lim.thy to Limits.thy
less more (0) -100 -60 tip