src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
2016-05-09 paulson 2016-05-09 lemmas about dimension, hyperplanes, span, etc.
2016-04-18 paulson 2016-04-18 numerous theorems about affine hulls, hyperplanes, etc.
2016-02-24 paulson 2016-02-24 Substantial new material for multivariate analysis. Also removal of some duplicates.
2016-01-11 immler 2016-01-11 generalized proofs
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-11-22 wenzelm 2015-11-22 more symbols;
2015-11-20 paulson 2015-11-20 Theory of homotopic paths (from HOL Light), plus comments and minor refinements
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-03 paulson 2015-09-03 new lemmas about vector_derivative, complex numbers, paths, etc.
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-08-05 wenzelm 2014-08-05 tuned proofs -- fewer warnings;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-03-25 hoelzl 2014-03-25 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
2014-03-18 huffman 2014-03-18 remove unnecessary finiteness assumptions from lemmas about setsum
2014-03-18 hoelzl 2014-03-18 cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
2014-03-18 immler 2014-03-18 removed dependencies on theory Ordered_Euclidean_Space
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-02-16 wenzelm 2014-02-16 tuned proofs;
2013-12-16 immler 2013-12-16 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-12 huffman 2013-09-12 prefer theorem name over 'long_thm_list(n)'
2013-09-12 huffman 2013-09-12 removed outdated comments
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-01-31 hoelzl 2013-01-31 simplify heine_borel type class
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-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-07 wenzelm 2012-09-07 tuned proofs;
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
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-01 huffman 2011-09-01 modernize lemmas about 'continuous' and 'continuous_on'; improve automation of continuity proofs;
2011-08-28 huffman 2011-08-28 move class perfect_space into RealVector.thy; use not_open_singleton as perfect_space class axiom; generalize some lemmas to class perfect_space;
2011-08-25 huffman 2011-08-25 rename subset_{interior,closure} to {interior,closure}_mono; remove some legacy theorem names;
2011-08-25 huffman 2011-08-25 simplify many proofs about subspace and span; reorder premises in rule span_induct;
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-22 huffman 2011-08-22 legacy theorem names
2011-08-21 huffman 2011-08-21 section -> subsection
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-15 huffman 2011-08-15 generalize lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq to class topological_space
2011-08-15 huffman 2011-08-15 add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;
2011-08-15 huffman 2011-08-15 remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-11 huffman 2011-08-11 avoid duplicate rule warnings
2011-08-11 huffman 2011-08-11 modify euclidean_space class to include basis set
2011-08-11 huffman 2011-08-11 remove lemma stupid_ext
2011-08-10 huffman 2011-08-10 remove several redundant and unused theorems about derivatives