src/HOL/Topological_Spaces.thy
Fri, 27 Sep 2013 09:26:31 +0200 Andreas Lochbihler add relator for 'a filter and parametricity theorems
Tue, 24 Sep 2013 15:03:49 -0700 huffman factor out new lemma
Tue, 24 Sep 2013 15:03:49 -0700 huffman replace lemma with more general simp rule
Tue, 03 Sep 2013 22:04:23 +0200 wenzelm tuned proofs -- less guessing;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 27 Aug 2013 14:37:56 +0200 hoelzl renamed typeclass dense_linorder to unbounded_dense_linorder
Thu, 25 Jul 2013 08:57:16 +0200 haftmann factored syntactic type classes for bot and top (by Alessandro Coglio)
Thu, 30 May 2013 23:29:33 +0200 wenzelm tuned headers;
Thu, 25 Apr 2013 11:59:21 +0200 hoelzl revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
Thu, 25 Apr 2013 10:35:56 +0200 hoelzl renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)
Wed, 24 Apr 2013 13:28:30 +0200 hoelzl spell conditional_ly_-complete lattices correct
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Tue, 26 Mar 2013 12:20:52 +0100 hoelzl separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
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 connected to HOL image; used to show intermediate value theorem
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
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)
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move first_countable_topology to the HOL image
Fri, 22 Mar 2013 10:41:42 +0100 hoelzl move topological_space to its own theory
less more (0) tip