src/HOL/Limits.thy
Mon, 12 Mar 2012 21:34:43 +0100 noschinl use eventually_elim method
Mon, 12 Mar 2012 21:28:10 +0100 noschinl add eventually_elim method
Thu, 15 Dec 2011 15:55:39 +0100 noschinl add lemmas about limits
Fri, 28 Oct 2011 23:41:16 +0200 wenzelm tuned Named_Thms: proper binding;
Tue, 20 Sep 2011 10:52:08 -0700 huffman add lemmas within_empty and tendsto_bot;
Wed, 31 Aug 2011 07:51:55 -0700 huffman convert to Isar-style proof
Sun, 28 Aug 2011 20:56:49 -0700 huffman move class perfect_space into RealVector.thy;
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Sat, 20 Aug 2011 06:34:51 -0700 huffman redefine constant 'trivial_limit' as an abbreviation
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Wed, 17 Aug 2011 11:39:09 -0700 huffman add lemma tendsto_compose_eventually; use it to shorten some proofs
Wed, 17 Aug 2011 11:06:39 -0700 huffman add lemma metric_tendsto_imp_tendsto
Mon, 15 Aug 2011 16:48:05 -0700 huffman add lemma tendsto_compose
Sun, 14 Aug 2011 10:47:47 -0700 huffman locale-ize some constant definitions, so complete_space can inherit from metric_space
Sun, 14 Aug 2011 10:25:43 -0700 huffman generalize constant 'lim' and limit uniqueness theorems to class t2_space
Sun, 14 Aug 2011 08:45:38 -0700 huffman consistently use variable name 'F' for filters
Sun, 14 Aug 2011 07:54:24 -0700 huffman generalize lemmas about LIM and LIMSEQ to tendsto
Mon, 08 Aug 2011 19:26:53 -0700 huffman rename type 'a net to 'a filter, following standard mathematical terminology
Mon, 08 Aug 2011 16:57:37 -0700 huffman remove duplicate lemmas
Mon, 14 Mar 2011 14:37:35 +0100 hoelzl generalize infinite sums
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Mon, 10 May 2010 21:33:48 -0700 huffman minimize imports
Tue, 04 May 2010 13:08:56 -0700 huffman generalize types of LIMSEQ and LIM; generalize many lemmas
Mon, 03 May 2010 18:40:48 -0700 huffman add lemmas eventually_nhds_metric and tendsto_mono
Mon, 03 May 2010 17:39:46 -0700 huffman remove unneeded premise
Mon, 03 May 2010 17:13:37 -0700 huffman add constants netmap and nhds
Sat, 01 May 2010 11:46:47 -0700 huffman complete_lattice instance for net type
Sat, 01 May 2010 09:43:40 -0700 huffman swap ordering on nets, so x <= y means 'x is finer than y'
Sun, 25 Apr 2010 20:48:19 -0700 huffman define finer-than ordering on net type; move some theorems into Limits.thy
Sun, 25 Apr 2010 11:58:39 -0700 huffman define nets directly as filters, instead of as filter bases
Thu, 02 Jul 2009 17:34:14 +0200 wenzelm renamed NamedThmsFun to Named_Thms;
Fri, 12 Jun 2009 15:46:21 -0700 huffman add lemma tendsto_setsum
Thu, 11 Jun 2009 11:51:12 -0700 huffman theorem attribute [tendsto_intros]
Sun, 07 Jun 2009 17:59:54 -0700 huffman replace 'topo' with 'open'; add extra type constraint for 'open'
Sat, 06 Jun 2009 09:11:12 -0700 huffman generalize tendsto to class topological_space
Fri, 05 Jun 2009 15:59:20 -0700 huffman put syntax for tendsto in Limits.thy; rename variables
Thu, 04 Jun 2009 17:24:09 -0700 huffman generalize type of 'at' to topological_space; generalize some lemmas
Tue, 02 Jun 2009 17:03:22 -0700 huffman replace filters with filter bases
Mon, 01 Jun 2009 16:27:54 -0700 huffman declare Bfun_def [code del]
Mon, 01 Jun 2009 10:56:31 -0700 huffman simp del -> code del
Mon, 01 Jun 2009 10:36:42 -0700 huffman limits of inverse using filters
Mon, 01 Jun 2009 07:57:37 -0700 huffman add [code del] declarations
Sun, 31 May 2009 21:59:33 -0700 huffman new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters
less more (0) tip