src/HOL/Series.thy
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
Mon, 03 May 2010 20:42:58 -0700 huffman remove unneeded constant Zseq
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Mon, 09 Nov 2009 19:42:33 +0100 wenzelm eliminated hard tabulators;
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Mon, 05 Oct 2009 17:27:46 +0100 paulson New lemmas connected with the reals and infinite series
Fri, 25 Sep 2009 13:47:28 +0100 paulson New lemmas involving the real numbers, especially limits and series
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
Sun, 22 Mar 2009 19:36:04 +0100 nipkow 1. New cancellation simprocs for common factors in inequations
Tue, 24 Feb 2009 11:12:58 -0800 huffman make more proofs work whether or not One_nat_def is a simp rule
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
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