src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
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)