src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
Tue, 05 Mar 2013 15:43:15 +0100 hoelzl continuity of pair operations
Tue, 05 Mar 2013 15:43:14 +0100 hoelzl use generate_topology for second countable topologies, does not require intersection stable basis
Tue, 05 Mar 2013 15:43:13 +0100 hoelzl generalized isGlb_unique
Wed, 13 Feb 2013 16:35:07 +0100 immler eliminated union_closed_basis; cleanup Fin_Map
Wed, 13 Feb 2013 16:35:07 +0100 immler fine grained instantiations
Wed, 13 Feb 2013 16:35:07 +0100 immler generalized
Wed, 13 Feb 2013 16:35:07 +0100 immler generalized
Thu, 31 Jan 2013 11:31:22 +0100 hoelzl simplify heine_borel type class
Fri, 18 Jan 2013 20:01:59 +0100 hoelzl generalized diameter from real_normed_vector to metric_space
Fri, 18 Jan 2013 20:01:41 +0100 hoelzl tuned proof
Fri, 18 Jan 2013 20:00:59 +0100 hoelzl tune prove compact_eq_totally_bounded
Thu, 17 Jan 2013 15:28:53 -0800 huffman generalized theorem edelstein_fix to class metric_space
Thu, 17 Jan 2013 08:31:16 -0800 huffman simplify proof of compact_imp_bounded
Tue, 15 Jan 2013 20:26:38 -0800 huffman generalize more topology lemmas
Tue, 15 Jan 2013 19:28:48 -0800 huffman generalize topology lemmas; simplify proofs
Thu, 17 Jan 2013 14:38:12 +0100 hoelzl simplified prove of compact_imp_bounded
Thu, 17 Jan 2013 13:58:02 +0100 hoelzl use accumulation point characterization (avoids t1_space restriction for equivalence of countable and sequential compactness); remove heine_borel_lemma
Thu, 17 Jan 2013 13:21:34 +0100 hoelzl move auxiliary lemma to top
Thu, 17 Jan 2013 13:20:17 +0100 hoelzl add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite
Thu, 17 Jan 2013 12:26:54 +0100 hoelzl group compactness-eq-seq-compactness lemmas together
Thu, 17 Jan 2013 12:21:24 +0100 hoelzl replace convergent_imp_cauchy by LIMSEQ_imp_Cauchy
Thu, 17 Jan 2013 12:09:48 +0100 hoelzl tuned
Thu, 17 Jan 2013 12:09:21 +0100 hoelzl removed subseq_bigger (replaced by seq_suble)
Thu, 17 Jan 2013 11:59:12 +0100 hoelzl countablility of finite subsets and rational numbers
Tue, 15 Jan 2013 08:29:56 -0800 huffman generalized more topology theorems
Mon, 14 Jan 2013 19:28:39 -0800 huffman generalize lemma islimpt_finite to class t1_space
Mon, 14 Jan 2013 18:30:36 +0100 hoelzl differentiate (cover) compactness and sequential compactness
Mon, 14 Jan 2013 17:53:37 +0100 hoelzl introduce first_countable_topology typeclass
Mon, 14 Jan 2013 17:30:36 +0100 hoelzl move prod instantiation of second_countable_topology to its definition
Mon, 14 Jan 2013 17:29:04 +0100 hoelzl renamed countable_basis_space to second_countable_topology
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
Mon, 03 Dec 2012 18:19:02 +0100 hoelzl add filterlim rules for diverging multiplication and addition; move at_infinity to the HOL image
Tue, 27 Nov 2012 13:48:40 +0100 immler based countable topological basis on Countable_Set
Fri, 16 Nov 2012 19:14:23 +0100 hoelzl moved (b)choice_iff(') to Hilbert_Choice
Fri, 16 Nov 2012 18:45:57 +0100 hoelzl move theorems to be more generally useable
Fri, 16 Nov 2012 11:22:22 +0100 immler allow arbitrary enumerations of basis in locale for generation of borel sets
Thu, 15 Nov 2012 10:49:58 +0100 immler regularity of measures, therefore:
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Fri, 05 Oct 2012 13:57: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, 31 May 2012 10:05:07 +0200 huffman remove stray reference to no-longer-existing theorem 'add'
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Mon, 12 Mar 2012 21:34:43 +0100 noschinl use eventually_elim method
Mon, 05 Dec 2011 15:10:15 +0100 huffman remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
Thu, 17 Nov 2011 18:31:00 +0100 huffman Groups.thy: generalize several lemmas from class ab_group_add to class group_add
Thu, 27 Oct 2011 07:46:57 +0200 huffman fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Tue, 20 Sep 2011 10:52:08 -0700 huffman add lemmas within_empty and tendsto_bot;
Mon, 12 Sep 2011 14:39:10 -0700 huffman shorten proof of frontier_straddle
Mon, 12 Sep 2011 11:54:20 -0700 huffman remove redundant lemma Lim_sequentially in favor of lemma LIMSEQ_def
Mon, 12 Sep 2011 10:43:36 -0700 huffman remove trivial lemma Lim_at_iff_LIM
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Fri, 02 Sep 2011 15:19:59 -0700 huffman simplify proof of Rats_dense_in_real;
Thu, 01 Sep 2011 10:41:19 -0700 huffman simplify some proofs about uniform continuity, and add some new ones;
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Wed, 31 Aug 2011 13:28:29 -0700 huffman simplify/generalize some proofs
Wed, 31 Aug 2011 08:11:47 -0700 huffman move lemmas from Topology_Euclidean_Space to Euclidean_Space
Mon, 29 Aug 2011 13:50:47 -0700 huffman simplify some proofs
Sun, 28 Aug 2011 20:56:49 -0700 huffman move class perfect_space into RealVector.thy;
less more (0) -100 -60 tip