src/HOL/Series.thy
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