| Thu, 17 Jan 2013 15:50:56 +0100 | wenzelm | merged | changeset | files |
| Thu, 17 Jan 2013 15:49:50 +0100 | wenzelm | tuned signature (again) -- keep Properties more generic; | changeset | files |
| Thu, 17 Jan 2013 15:17:48 +0100 | wenzelm | tuned proofs; | changeset | files |
| Thu, 17 Jan 2013 14:38:12 +0100 | hoelzl | simplified prove of compact_imp_bounded | changeset | files |
| 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 | changeset | files |
| Thu, 17 Jan 2013 13:21:34 +0100 | hoelzl | move auxiliary lemma to top | changeset | files |
| Thu, 17 Jan 2013 13:20:17 +0100 | hoelzl | add countable compacteness; replace finite_range_imp_infinite_repeats by pigeonhole_infinite | changeset | files |