Mon, 15 Aug 2011 14:09:39 -0700 add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman [Mon, 15 Aug 2011 14:09:39 -0700] rev 44213
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq; simplify and generalize some proofs;
Mon, 15 Aug 2011 12:18:34 -0700 generalize lemma continuous_uniform_limit to class metric_space
huffman [Mon, 15 Aug 2011 12:18:34 -0700] rev 44212
generalize lemma continuous_uniform_limit to class metric_space
Mon, 15 Aug 2011 12:13:46 -0700 remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
huffman [Mon, 15 Aug 2011 12:13:46 -0700] rev 44211
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
Mon, 15 Aug 2011 10:49:48 -0700 Topology_Euclidean_Space.thy: organize section headings
huffman [Mon, 15 Aug 2011 10:49:48 -0700] rev 44210
Topology_Euclidean_Space.thy: organize section headings
Mon, 15 Aug 2011 09:08:17 -0700 simplify some proofs
huffman [Mon, 15 Aug 2011 09:08:17 -0700] rev 44209
simplify some proofs
Sun, 14 Aug 2011 13:04:57 -0700 generalize lemma convergent_subseq_convergent
huffman [Sun, 14 Aug 2011 13:04:57 -0700] rev 44208
generalize lemma convergent_subseq_convergent
Sun, 14 Aug 2011 11:44:12 -0700 locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
huffman [Sun, 14 Aug 2011 11:44:12 -0700] rev 44207
locale-ize some definitions, so perfect_space and heine_borel can inherit from the proper superclasses
Sun, 14 Aug 2011 10:47:47 -0700 locale-ize some constant definitions, so complete_space can inherit from metric_space
huffman [Sun, 14 Aug 2011 10:47:47 -0700] rev 44206
locale-ize some constant definitions, so complete_space can inherit from metric_space
Sun, 14 Aug 2011 10:25:43 -0700 generalize constant 'lim' and limit uniqueness theorems to class t2_space
huffman [Sun, 14 Aug 2011 10:25:43 -0700] rev 44205
generalize constant 'lim' and limit uniqueness theorems to class t2_space
Tue, 16 Aug 2011 07:17:15 +0900 Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Aug 2011 07:17:15 +0900] rev 44204
Quotient Package: make quotient_type work with separate set type
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip