Tue, 04 May 2010 13:08:56 -0700 | huffman | generalize types of LIMSEQ and LIM; generalize many lemmas | changeset | files |
Tue, 04 May 2010 10:42:47 -0700 | huffman | make (f -- a --> x) an abbreviation for (f ---> x) (at a) | changeset | files |
Tue, 04 May 2010 10:06:05 -0700 | huffman | make (X ----> L) an abbreviation for (X ---> L) sequentially | changeset | files |
Tue, 04 May 2010 09:56:34 -0700 | huffman | adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2) | changeset | files |