src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
2014-03-18 immler 2014-03-18 use cbox to relax class constraints
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-03-13 huffman 2014-03-13 remove ordered_euclidean_space constraint from brouwer/derivative lemmas; add constant unit_cube for class euclidean_space
2014-02-16 wenzelm 2014-02-16 tuned proofs;
2014-02-14 wenzelm 2014-02-14 tuned proofs;
2013-12-16 immler 2013-12-16 prefer box over greaterThanLessThan on euclidean_space
2013-09-24 wenzelm 2013-09-24 tuned proofs;
2013-09-18 wenzelm 2013-09-18 tuned proofs;
2013-09-17 wenzelm 2013-09-17 tuned proofs;
2013-08-28 wenzelm 2013-08-28 tuned proofs;
2013-08-28 wenzelm 2013-08-28 tuned proofs;
2013-08-24 wenzelm 2013-08-24 tuned proofs;
2013-08-24 wenzelm 2013-08-24 tuned proofs;
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-01-14 hoelzl 2013-01-14 differentiate (cover) compactness and sequential compactness
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-12 blanchet 2012-12-12 tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
2012-11-08 bulwahn 2012-11-08 adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
2012-09-24 wenzelm 2012-09-24 tuned proofs;
2012-09-14 wenzelm 2012-09-14 tuned proofs;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-07 huffman 2011-09-07 avoid using legacy theorem names
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-03-13 wenzelm 2011-03-13 eliminated hard tabs;
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-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-04-28 huffman 2010-04-28 remove redundant lemma vector_dist_norm
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-25 huffman 2010-04-25 simplify types of path operations (use real instead of real^1)
2010-04-24 huffman 2010-04-24 document generation for Multivariate_Analysis
2010-04-23 wenzelm 2010-04-23 eliminated spurious schematic statements;
2010-03-11 haftmann 2010-03-11 replaced card_def by card_eq_setsum
2010-01-25 hoelzl 2010-01-25 Replaced vec1 and dest_vec1 by abbreviation.
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-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.
2009-11-17 hoelzl 2009-11-17 Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)