src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
2016-01-05 wenzelm 2016-01-05 tuned;
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-25 wenzelm 2015-06-25 tuned proofs;
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-10 wenzelm 2015-06-10 misc tuning;
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-03-20 paulson 2015-03-20 tweaked a few slow or very ugly proofs
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-14 hoelzl 2014-04-14 added divide_nonneg_nonneg and co; made it a simp rule
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-25 hoelzl 2014-03-25 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
2014-03-20 huffman 2014-03-20 generalize some theorems
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.