src/HOL/Limits.thy
2009-06-12 huffman 2009-06-12 add lemma tendsto_setsum
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-06 huffman 2009-06-06 generalize tendsto to class topological_space
2009-06-05 huffman 2009-06-05 put syntax for tendsto in Limits.thy; rename variables
2009-06-04 huffman 2009-06-04 generalize type of 'at' to topological_space; generalize some lemmas
2009-06-02 huffman 2009-06-02 replace filters with filter bases
2009-06-01 huffman 2009-06-01 declare Bfun_def [code del]
2009-06-01 huffman 2009-06-01 simp del -> code del
2009-06-01 huffman 2009-06-01 limits of inverse using filters
2009-06-01 huffman 2009-06-01 add [code del] declarations
2009-05-31 huffman 2009-05-31 new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters