src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
Fri, 15 Jul 2016 12:17:16 +0200 hoelzl HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
Thu, 14 Jul 2016 16:49:22 +0100 paulson Got rid of the \nexists macro
Thu, 14 Jul 2016 14:48:49 +0100 paulson More advanced theorems about retracts, homotopies., etc
Wed, 13 Jul 2016 17:14:17 +0100 paulson lots of new theorems about differentiable_on, retracts, ANRs, etc.
Sat, 02 Jul 2016 08:41:05 +0200 haftmann more theorems
Wed, 15 Jun 2016 22:19:03 +0200 hoelzl move open_Collect_eq/less to HOL
Thu, 16 Jun 2016 12:05:04 +0100 paulson Removed instances of ^ from theory markup
Wed, 15 Jun 2016 15:52:24 +0100 paulson Urysohn's lemma, Dugundji extension theorem and many other proofs
Tue, 14 Jun 2016 15:34:21 +0100 paulson new results about topology
Tue, 24 May 2016 15:08:07 +0100 paulson Merge
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 11 Apr 2016 16:27:42 +0100 paulson lots of new theorems for multivariate analysis
Mon, 04 Apr 2016 16:52:56 +0100 paulson Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
Tue, 23 Feb 2016 18:04:31 +0100 nipkow resolved conflict
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Tue, 23 Feb 2016 15:47:39 +0000 paulson New and revised material for (multivariate) analysis
Tue, 05 Jan 2016 15:35:08 +0100 wenzelm tuned;
Mon, 28 Dec 2015 01:28:28 +0100 wenzelm more symbols;
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Tue, 27 Oct 2015 15:17:02 +0000 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
Wed, 30 Sep 2015 16:36:42 +0100 paulson real_of_nat_Suc is now a simprule
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Thu, 25 Jun 2015 23:33:47 +0200 wenzelm tuned proofs;
Sat, 13 Jun 2015 13:09:05 +0200 wenzelm renamed "prems" to "that";
Wed, 10 Jun 2015 20:15:58 +0200 wenzelm misc tuning;
Wed, 10 Jun 2015 19:10:20 +0200 wenzelm isabelle update_cartouches;
Tue, 26 May 2015 21:58:04 +0100 paulson New material about paths, and some lemmas
Fri, 20 Mar 2015 16:11:28 +0000 paulson tweaked a few slow or very ugly proofs
Sun, 02 Nov 2014 17:09:04 +0100 wenzelm modernized header;
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Mon, 14 Apr 2014 13:08:17 +0200 hoelzl added divide_nonneg_nonneg and co; made it a simp rule
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Fri, 11 Apr 2014 22:53:33 +0200 nipkow made divide_pos_pos a simp rule
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Tue, 25 Mar 2014 14:20:58 +0100 hoelzl cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
Thu, 20 Mar 2014 09:21:39 -0700 huffman generalize some theorems
Tue, 18 Mar 2014 10:12:57 +0100 immler use cbox to relax class constraints
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Thu, 13 Mar 2014 16:07:27 -0700 huffman remove ordered_euclidean_space constraint from brouwer/derivative lemmas;
Sun, 16 Feb 2014 21:09:47 +0100 wenzelm tuned proofs;
Fri, 14 Feb 2014 16:11:14 +0100 wenzelm tuned proofs;
Mon, 16 Dec 2013 17:08:22 +0100 immler prefer box over greaterThanLessThan on euclidean_space
Tue, 24 Sep 2013 17:37:45 +0200 wenzelm tuned proofs;
Wed, 18 Sep 2013 00:11:15 +0200 wenzelm tuned proofs;
Tue, 17 Sep 2013 00:13:20 +0200 wenzelm tuned proofs;
Wed, 28 Aug 2013 22:50:23 +0200 wenzelm tuned proofs;
Wed, 28 Aug 2013 17:20:16 +0200 wenzelm tuned proofs;
Sat, 24 Aug 2013 23:16:37 +0200 wenzelm tuned proofs;
Sat, 24 Aug 2013 21:23:40 +0200 wenzelm tuned proofs;
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl 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)
Mon, 14 Jan 2013 18:30:36 +0100 hoelzl differentiate (cover) compactness and sequential compactness
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Wed, 12 Dec 2012 22:37:06 +0100 blanchet tuned two lemma names, to avoid name hint clash (which confuses the MaSh evaluation, and which anyway isn't nice or necessary)
Thu, 08 Nov 2012 11:59:48 +0100 bulwahn adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
Mon, 24 Sep 2012 17:52:44 +0200 wenzelm tuned proofs;
Fri, 14 Sep 2012 21:26:01 +0200 wenzelm tuned proofs;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
less more (0) -60 tip