src/HOL/Deriv.thy
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Wed, 31 Oct 2018 15:53:32 +0100 wenzelm clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
Wed, 03 Oct 2018 10:42:00 +0100 paulson merged
Mon, 24 Sep 2018 14:33:08 +0100 paulson cosmetic change to mvt
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
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
Mon, 16 Jul 2018 23:33:28 +0100 paulson de-applying and simplifying proofs
Sun, 15 Jul 2018 21:58:50 +0100 paulson de-applying and meta-quantifying
Sun, 15 Jul 2018 16:05:38 +0100 paulson fixes and more de-applying
Sun, 15 Jul 2018 13:15:31 +0100 paulson more de-applying and a fix
Tue, 10 Jul 2018 23:18:08 +0100 paulson de-applying, etc.
Sat, 07 Jul 2018 15:07:37 +0100 paulson de-applying, etc.
Thu, 28 Jun 2018 14:13:57 +0100 paulson Generalising and renaming some basic results
Fri, 23 Feb 2018 14:56:32 +0000 Wenda Li merged
Fri, 23 Feb 2018 13:27:19 +0000 Wenda Li Unified the order of zeros and poles; improved reasoning around non-essential singularites
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Tue, 16 Jan 2018 09:30:00 +0100 wenzelm standardized towards new-style formal comments: isabelle update_comments;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Wed, 06 Dec 2017 20:43:09 +0100 wenzelm prefer control symbol antiquotations;
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
less more (0) -100 -60 tip