src/HOL/Lim.thy
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
Tue, 16 Aug 2011 09:31:23 -0700 huffman add simp rules for isCont
Mon, 15 Aug 2011 16:48:05 -0700 huffman add lemma tendsto_compose
Mon, 15 Aug 2011 16:18:13 -0700 huffman remove extraneous subsection heading
Sun, 14 Aug 2011 10:25:43 -0700 huffman generalize constant 'lim' and limit uniqueness theorems to class t2_space
Sun, 14 Aug 2011 07:54:24 -0700 huffman generalize lemmas about LIM and LIMSEQ to tendsto
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 04 May 2010 15:44:42 -0700 huffman generalize more lemmas about limits
Tue, 04 May 2010 13:08:56 -0700 huffman generalize types of LIMSEQ and LIM; generalize many lemmas
Tue, 04 May 2010 10:42:47 -0700 huffman make (f -- a --> x) an abbreviation for (f ---> x) (at a)
Wed, 23 Sep 2009 13:17:17 +0200 hoelzl correct variable order in approximate-method
Tue, 22 Sep 2009 15:36:55 +0200 haftmann be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
Fri, 28 Aug 2009 18:52:41 +0200 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
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
Tue, 02 Jun 2009 17:03:22 -0700 huffman replace filters with filter bases
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
Fri, 29 May 2009 09:22:56 -0700 huffman generalize constants from Lim.thy to class metric_space
Thu, 28 May 2009 22:57:17 -0700 huffman generalize constants in SEQ.thy to class metric_space
Tue, 28 Apr 2009 15:50:30 +0200 haftmann stripped class recpower further
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Thu, 12 Feb 2009 20:36:41 -0800 huffman add lemmas about sgn
Thu, 05 Feb 2009 11:34:42 +0100 hoelzl Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
Wed, 28 Jan 2009 16:29:16 +0100 nipkow Replaced group_ and ring_simps by algebra_simps;
Mon, 29 Dec 2008 14:08:08 +0100 haftmann adapted HOL source structure to distribution layout
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
less more (0) tip