src/HOL/Multivariate_Analysis/Derivative.thy
2013-03-22 hoelzl 2013-03-22 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)
2013-03-06 hoelzl 2013-03-06 changed has_derivative_intros into a named theorems collection
2013-01-17 hoelzl 2013-01-17 replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-12-07 hoelzl 2012-12-07 fundamental theorem of calculus for the Lebesgue integral
2012-03-13 wenzelm 2012-03-13 tuned proofs -- eliminated pointless chaining of facts after 'interpret';
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-20 huffman 2011-09-20 add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;
2011-09-12 huffman 2011-09-12 remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-25 huffman 2011-08-25 replace some continuous_on lemmas with more general versions
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-10 huffman 2011-08-10 remove several redundant and unused theorems about derivatives
2011-08-10 huffman 2011-08-10 simplify some proofs
2011-08-09 huffman 2011-08-09 mark some redundant theorems as legacy
2011-08-09 huffman 2011-08-09 Derivative.thy: more sensible subsection headings
2011-08-09 huffman 2011-08-09 Derivative.thy: clean up formatting
2011-08-08 huffman 2011-08-08 rename type 'a net to 'a filter, following standard mathematical terminology
2011-06-09 hoelzl 2011-06-09 lemmas about right derivative and limits
2011-03-14 hoelzl 2011-03-14 generalize infinite sums
2011-03-13 wenzelm 2011-03-13 eliminated hard tabs;
2011-02-22 hoelzl 2011-02-22 add name continuous_isCont to unnamed lemma
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-04 huffman 2010-07-04 generalize some lemmas about derivatives
2010-06-30 huffman 2010-06-30 generalize some lemmas about derivatives
2010-06-30 huffman 2010-06-30 generalize more euclidean_space lemmas
2010-06-28 haftmann 2010-06-28 inner_simps is not enough, need also local facts
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-05-11 hoelzl 2010-05-11 Removed usage of normalizating locales.
2010-05-07 haftmann 2010-05-07 prefix normalizing replaces class_semiring
2010-05-06 haftmann 2010-05-06 former free-floating field_comp_conv now in structure Normalizer
2010-04-29 huffman 2010-04-29 define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-28 huffman 2010-04-28 remove redundant lemma vector_dist_norm
2010-04-28 huffman 2010-04-28 move operator norm stuff to new theory file
2010-04-26 huffman 2010-04-26 more lemmas to Vec1.thy
2010-04-26 huffman 2010-04-26 simplify proof
2010-04-26 huffman 2010-04-26 move more lemmas into Vec1.thy
2010-04-26 huffman 2010-04-26 move proof of Fashoda meet theorem into separate file
2010-04-26 huffman 2010-04-26 move definitions and theorems for type real^1 to separate theory file
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix lots of looping simp calls and other warnings
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-04-24 huffman 2010-04-24 document generation for Multivariate_Analysis
2010-03-02 himmelma 2010-03-02 replaced \<bullet> with inner
2010-02-18 himmelma 2010-02-18 Equivalence between DERIV and one-dimensional derivation in Multivariate-Analysis
2010-02-17 himmelma 2010-02-17 Added integration to Multivariate-Analysis (upto FTC)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-01 himmelma 2010-02-01 Removed explicit type annotations
2010-01-25 hoelzl 2010-01-25 Replaced vec1 and dest_vec1 by abbreviation.
2010-01-15 haftmann 2010-01-15 spurious proof failure
2010-01-07 hoelzl 2010-01-07 finite annotation on cartesian product is now implicit.
2010-01-06 himmelma 2010-01-06 Made finite cartesian products finite
2009-11-29 huffman 2009-11-29 make proof use only abstract properties of eventually
2009-11-19 hoelzl 2009-11-19 Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
2009-11-19 hoelzl 2009-11-19 Renamed vector_less_eq_def to the more usual name vector_le_def.