isabelle: File revisions

src/HOL/Limits.thy

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

isabelle