huffman [Sun, 31 May 2009 11:27:19 -0700] rev 31348
more abstract properties of eventually
huffman [Sun, 31 May 2009 10:59:46 -0700] rev 31347
new lemmas about eventually; rewrite Lim proofs to use more abstract properties of eventually
huffman [Fri, 29 May 2009 22:42:13 -0700] rev 31346
generalize at function to class perfect_space
huffman [Fri, 29 May 2009 18:23:07 -0700] rev 31345
generalize topological notions to class metric_space; add class perfect_space
huffman [Fri, 29 May 2009 15:32:33 -0700] rev 31344
instance ^ :: (metric_space, finite) metric_space
huffman [Fri, 29 May 2009 14:09:58 -0700] rev 31343
generalize tendsto and related constants to class metric_space
huffman [Fri, 29 May 2009 10:31:35 -0700] rev 31342
add lemmas Lim_at_iff_LIM, Lim_sequentially_iff_LIMSEQ