huffman [Mon, 15 Aug 2011 16:48:05 -0700] rev 44218
add lemma tendsto_compose
huffman [Mon, 15 Aug 2011 16:18:13 -0700] rev 44217
remove extraneous subsection heading
huffman [Mon, 15 Aug 2011 15:11:55 -0700] rev 44216
generalized lemma closed_Collect_eq
huffman [Mon, 15 Aug 2011 14:50:24 -0700] rev 44215
remove duplicate lemma disjoint_iff
huffman [Mon, 15 Aug 2011 14:29:17 -0700] rev 44214
Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
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;
huffman [Mon, 15 Aug 2011 12:18:34 -0700] rev 44212
generalize lemma continuous_uniform_limit to class metric_space
huffman [Mon, 15 Aug 2011 12:13:46 -0700] rev 44211
remove duplicate lemmas eventually_conjI, eventually_and, eventually_false
huffman [Mon, 15 Aug 2011 10:49:48 -0700] rev 44210
Topology_Euclidean_Space.thy: organize section headings
huffman [Mon, 15 Aug 2011 09:08:17 -0700] rev 44209
simplify some proofs