src/HOL/Multivariate_Analysis/Path_Connected.thy
Mon, 23 May 2016 16:03:29 +0100 paulson deleted stray thm command
Mon, 23 May 2016 16:02:46 +0100 paulson deleted needless comment
Mon, 23 May 2016 15:33:24 +0100 paulson Lots of new material for multivariate analysis
Fri, 13 May 2016 20:24:10 +0200 wenzelm eliminated use of empty "assms";
Mon, 25 Apr 2016 16:09:26 +0200 wenzelm eliminated old 'def';
Mon, 18 Apr 2016 15:40:55 +0100 paulson numerous theorems about affine hulls, hyperplanes, etc.
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
Wed, 16 Mar 2016 13:57:06 +0000 paulson Contractible sets. Also removal of obsolete theorems and refactoring
Mon, 14 Mar 2016 15:58:02 +0000 paulson New results about paths, segments, etc. The notion of simply_connected.
Mon, 14 Mar 2016 14:19:06 +0000 paulson Refactoring (moving theorems into better locations), plus a bit of new material
Mon, 07 Mar 2016 14:34:45 +0000 paulson new material to Blochj's theorem, as well as supporting lemmas
Wed, 24 Feb 2016 16:00:57 +0000 paulson Merge
Wed, 24 Feb 2016 15:51:01 +0000 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
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
Thu, 07 Jan 2016 17:40:55 +0000 paulson revisions to limits and derivatives, plus new lemmas
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Mon, 07 Dec 2015 16:44:26 +0000 paulson Cauchy's integral formula for circles. Starting to fix eventually_mono.
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Mon, 23 Nov 2015 16:57:54 +0000 paulson New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
Fri, 20 Nov 2015 14:44:53 +0000 paulson Theory of homotopic paths (from HOL Light), plus comments and minor refinements
Wed, 18 Nov 2015 15:23:34 +0000 paulson New theorems mostly from Peter Gammie
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Mon, 26 Oct 2015 23:41:27 +0000 paulson new lemmas about topology, etc., for Cauchy integral formula
Tue, 13 Oct 2015 12:42:08 +0100 paulson new material on path_component_sets, inside, outside, etc. And more default simprules
Mon, 21 Sep 2015 19:52:13 +0100 paulson new lemmas and movement of lemmas into place
Wed, 19 Aug 2015 19:18:19 +0100 paulson New material and fixes related to the forthcoming Stone-Weierstrass development
Tue, 28 Jul 2015 16:16:13 +0100 paulson the Cauchy integral theorem and related material
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
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Sun, 02 Nov 2014 17:09:04 +0100 wenzelm modernized header;
Wed, 02 Apr 2014 18:35:07 +0200 hoelzl extend continuous_intros; remove continuous_on_intros and isCont_intros
Tue, 18 Mar 2014 10:12:57 +0100 immler use cbox to relax class constraints
Sat, 14 Sep 2013 23:52:36 +0200 wenzelm tuned proofs;
Thu, 12 Sep 2013 09:03:52 -0700 huffman removed outdated comments
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
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)
Thu, 17 Jan 2013 11:57:17 +0100 hoelzl generalize compact_path_image to topological_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
Fri, 28 Sep 2012 23:45:15 +0200 wenzelm tuned proofs;
Fri, 28 Sep 2012 23:40:48 +0200 wenzelm tuned proofs;
Mon, 25 Jun 2012 17:41:20 +0200 wenzelm tuned proofs -- prefer direct "rotated" instead of old-style COMP;
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Thu, 01 Jul 2010 15:40:38 -0700 huffman convert theorem path_connected_sphere to euclidean_space class
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Wed, 28 Apr 2010 16:11:07 -0700 huffman move path-related stuff into new theory file
less more (0) tip