Sun, 07 Jun 2009 12:00:03 -0700 | huffman | move definitions of open, closed to RealVector.thy | changeset | files |
Sat, 06 Jun 2009 10:28:34 -0700 | huffman | lemmas islimptI, islimptE; generalize open_inter_closure_subset | changeset | files |
Sat, 06 Jun 2009 09:11:12 -0700 | huffman | generalize tendsto to class topological_space | changeset | files |