src/HOL/Series.thy
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Fri, 30 May 2014 14:55:10 +0200 hoelzl introduce more powerful reindexing rules for big operators
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Fri, 11 Apr 2014 13:36:57 +0200 nipkow made mult_nonneg_nonneg a simp rule
Wed, 02 Apr 2014 18:35:01 +0200 hoelzl moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Wed, 19 Mar 2014 17:06:02 +0000 paulson Some rationalisation of basic lemmas
Wed, 19 Mar 2014 15:34:57 +0100 hoelzl further renaming in Series
Tue, 18 Mar 2014 16:29:32 +0100 hoelzl fix HOL-NSA; move lemmas
Tue, 18 Mar 2014 15:53:48 +0100 hoelzl cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
Mon, 17 Mar 2014 15:48:30 +0000 paulson a few new theorems
Mon, 09 Dec 2013 12:22:23 +0100 wenzelm more antiquotations;
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Fri, 13 Sep 2013 07:59:50 +0200 haftmann tuned proofs
Tue, 26 Mar 2013 12:20:59 +0100 hoelzl Series.thy is based on Limits.thy and not Deriv.thy
Tue, 26 Mar 2013 12:20:58 +0100 hoelzl move SEQ.thy and Lim.thy to Limits.thy
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl clean up lemma_nest_unique and renamed to nested_sequence_unique
Thu, 31 Jan 2013 11:31:27 +0100 hoelzl introduce order topology
Mon, 03 Dec 2012 18:19:12 +0100 hoelzl use filterlim in Lim and SEQ; tuned proofs
Wed, 25 Apr 2012 19:26:00 +0200 hoelzl moved lemmas to appropriate places
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 13 Mar 2012 16:40:06 +0100 wenzelm prefer abs_def over def_raw;
Mon, 05 Sep 2011 16:26:57 -0700 huffman modify lemma sums_group, and shorten proofs that use it
Mon, 05 Sep 2011 16:07:40 -0700 huffman generalize some lemmas
Sun, 04 Sep 2011 09:49:45 -0700 huffman remove redundant lemmas about LIMSEQ
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Thu, 18 Aug 2011 19:53:03 -0700 huffman optimize some proofs
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Mon, 14 Mar 2011 14:37:35 +0100 hoelzl generalize infinite sums
Tue, 04 May 2010 10:06:05 -0700 huffman make (X ----> L) an abbreviation for (X ---> L) sequentially
less more (0) -30 tip