| Mon, 01 Jun 2009 10:02:01 +0200 | nipkow | new lemma | changeset | files |
| Sun, 31 May 2009 22:00:56 -0700 | huffman | merged | changeset | files |
| Sun, 31 May 2009 21:59:33 -0700 | huffman | new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters | changeset | files |
| Sun, 31 May 2009 11:27:19 -0700 | huffman | more abstract properties of eventually | changeset | files |
| Sun, 31 May 2009 10:59:46 -0700 | huffman | new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually | changeset | files |
| Fri, 29 May 2009 22:42:13 -0700 | huffman | generalize at function to class perfect_space | changeset | files |
| Fri, 29 May 2009 18:23:07 -0700 | huffman | generalize topological notions to class metric_space; add class perfect_space | changeset | files |
| Fri, 29 May 2009 15:32:33 -0700 | huffman | instance ^ :: (metric_space, finite) metric_space | changeset | files |