src/HOL/SEQ.thy
Mon, 22 Feb 2010 20:41:49 +0100 hoelzl Replaced Integration by Multivariate-Analysis/Real_Integration
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Wed, 28 Oct 2009 11:42:31 +0000 paulson New theory Probability, which contains a development of measure theory
Wed, 21 Oct 2009 12:02:56 +0200 haftmann curried union as canonical list operation
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
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
Fri, 28 Aug 2009 18:52:41 +0200 nipkow Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
Tue, 14 Jul 2009 15:54:19 +0200 haftmann refinement of lattice classes
Fri, 12 Jun 2009 15:46:21 -0700 huffman add lemma tendsto_setsum
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 23:31:03 -0700 huffman generalize type of constant lim
Tue, 02 Jun 2009 23:06:05 -0700 huffman class complete_space
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
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
Thu, 26 Mar 2009 14:10:48 +0000 paulson New theorems mostly concerning infinite series.
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Mon, 02 Mar 2009 12:33:12 +0000 chaieb Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy
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
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
less more (0) tip