src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-07-15 hoelzl 2016-07-15 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
2016-07-14 paulson 2016-07-14 Got rid of the \nexists macro
2016-07-14 paulson 2016-07-14 More advanced theorems about retracts, homotopies., etc
2016-07-13 paulson 2016-07-13 lots of new theorems about differentiable_on, retracts, ANRs, etc.
2016-07-02 haftmann 2016-07-02 more theorems
2016-06-15 hoelzl 2016-06-15 move open_Collect_eq/less to HOL
2016-06-16 paulson 2016-06-16 Removed instances of ^ from theory markup
2016-06-15 paulson 2016-06-15 Urysohn's lemma, Dugundji extension theorem and many other proofs
2016-06-14 paulson 2016-06-14 new results about topology
2016-05-24 paulson 2016-05-24 Merge
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-11 paulson 2016-04-11 lots of new theorems for multivariate analysis
2016-04-04 paulson 2016-04-04 Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-02-23 nipkow 2016-02-23 resolved conflict
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-23 paulson 2016-02-23 New and revised material for (multivariate) analysis
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