Tue, 09 Jun 2009 10:23:41 -0700 | huffman | instance heine_borel < complete_space; generalize many lemmas to class heine_borel | changeset | files |
Tue, 09 Jun 2009 09:38:56 -0700 | huffman | new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^ | changeset | files |
Mon, 08 Jun 2009 19:45:24 -0700 | huffman | generalize compact/closure lemmas | changeset | files |