src/HOL/Multivariate_Analysis/Derivative.thy
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Mon, 16 Jun 2014 17:52:33 +0200 hoelzl add more derivative and continuity rules for complex-values functions
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Sun, 06 Apr 2014 21:01:33 +0200 nipkow tuned lemmas: more general class
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:02 +0200 hoelzl reorder Complex_Analysis_Basics; rename DD to deriv
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Mon, 31 Mar 2014 17:17:37 +0200 hoelzl tuned proofs
Fri, 28 Mar 2014 18:21:07 -0700 huffman tuned proofs
Mon, 24 Mar 2014 14:51:10 -0700 huffman generalized theorems about derivatives of limits of sequences of funtions
Thu, 20 Mar 2014 17:55:33 -0700 huffman tuned proofs
Mon, 24 Mar 2014 14:22:29 +0000 paulson rearranging some deriv theorems
Thu, 20 Mar 2014 15:13:55 -0700 huffman generalize more theorems
Thu, 20 Mar 2014 09:21:39 -0700 huffman generalize some theorems
Wed, 19 Mar 2014 20:50:24 -0700 huffman generalize theory of operator norms to work with class real_normed_vector
Wed, 19 Mar 2014 17:06:02 +0000 paulson Some rationalisation of basic lemmas
Tue, 18 Mar 2014 09:39:07 -0700 huffman remove unnecessary finiteness assumptions from lemmas about setsum
Tue, 18 Mar 2014 15:53:48 +0100 hoelzl cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
Tue, 18 Mar 2014 10:12:57 +0100 immler use cbox to relax class constraints
Mon, 17 Mar 2014 20:38:50 +0100 hoelzl remove sums_seq, it is not used
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, 14 Mar 2014 13:27:38 -0700 huffman add lemmas about nhds filter; tuned proof
Fri, 14 Mar 2014 10:59:43 -0700 huffman remove unused lemma which was a direct consequence of tendsto_intros
Fri, 14 Mar 2014 09:09:33 -0700 huffman generalization of differential_zero_maxmin to class real_normed_vector
Thu, 13 Mar 2014 16:07:27 -0700 huffman remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
Fri, 07 Mar 2014 15:52:56 +0000 paulson Some new proofs. Tidying up, esp to remove "apply rule".
Fri, 21 Feb 2014 23:42:43 +0100 wenzelm tuned proofs;
Mon, 16 Dec 2013 17:08:22 +0100 immler prefer box over greaterThanLessThan on euclidean_space
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Mon, 23 Sep 2013 13:34:15 +0200 wenzelm proper text for document preparation;
Sat, 21 Sep 2013 22:33:42 +0200 wenzelm tuned proofs;
Thu, 12 Sep 2013 18:09:17 -0700 huffman make 'linear' into a sublocale of 'bounded_linear';
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Sun, 18 Aug 2013 19:59:19 +0200 wenzelm more symbols;
Mon, 22 Apr 2013 18:39:12 +0200 immler removed type constraints
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)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
Wed, 06 Mar 2013 16:56:21 +0100 hoelzl changed has_derivative_intros into a named theorems collection
Thu, 17 Jan 2013 12:21:24 +0100 hoelzl replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Fri, 07 Dec 2012 14:29:08 +0100 hoelzl fundamental theorem of calculus for the Lebesgue integral
Tue, 13 Mar 2012 13:31:26 +0100 wenzelm tuned proofs -- eliminated pointless chaining of facts after 'interpret';
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
Tue, 20 Sep 2011 10:52:08 -0700 huffman add lemmas within_empty and tendsto_bot;
Mon, 12 Sep 2011 11:54:20 -0700 huffman remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Wed, 10 Aug 2011 16:35:50 -0700 huffman remove several redundant and unused theorems about derivatives
Wed, 10 Aug 2011 14:10:52 -0700 huffman simplify some proofs
Tue, 09 Aug 2011 10:30:00 -0700 huffman mark some redundant theorems as legacy
Tue, 09 Aug 2011 08:53:12 -0700 huffman Derivative.thy: more sensible subsection headings
Tue, 09 Aug 2011 07:37:18 -0700 huffman Derivative.thy: clean up formatting
less more (0) -60 tip