Sun, 04 Sep 2011 11:16:47 0700 
huffman 
simplify proof of Bseq_mono_convergent

file 
diff 
annotate

Sun, 04 Sep 2011 09:49:45 0700 
huffman 
remove redundant lemmas about LIMSEQ

file 
diff 
annotate

Sun, 28 Aug 2011 09:20:12 0700 
huffman 
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems

file 
diff 
annotate

Fri, 19 Aug 2011 15:07:10 0700 
huffman 
SEQ.thy: legacy theorem names

file 
diff 
annotate

Thu, 18 Aug 2011 13:36:58 0700 
huffman 
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas

file 
diff 
annotate

Sun, 14 Aug 2011 13:04:57 0700 
huffman 
generalize lemma convergent_subseq_convergent

file 
diff 
annotate

Sun, 14 Aug 2011 10:47:47 0700 
huffman 
localeize some constant definitions, so complete_space can inherit from metric_space

file 
diff 
annotate

Sun, 14 Aug 2011 10:25:43 0700 
huffman 
generalize constant 'lim' and limit uniqueness theorems to class t2_space

file 
diff 
annotate

Sun, 14 Aug 2011 07:54:24 0700 
huffman 
generalize lemmas about LIM and LIMSEQ to tendsto

file 
diff 
annotate

Mon, 14 Mar 2011 14:37:37 +0100 
hoelzl 
add lemmas for monotone sequences

file 
diff 
annotate

Tue, 21 Dec 2010 14:50:53 +0100 
hoelzl 
generalized monoseq, decseq and incseq; simplified proof for seq_monosub

file 
diff 
annotate

Tue, 30 Nov 2010 08:58:47 0800 
huffman 
simplify proof of LIMSEQ_unique

file 
diff 
annotate

Mon, 19 Jul 2010 16:09:44 +0200 
haftmann 
diff_minus subsumes diff_def

file 
diff 
annotate

Mon, 12 Jul 2010 10:48:37 +0200 
haftmann 
dropped superfluous [code del]s

file 
diff 
annotate

Mon, 10 May 2010 21:33:48 0700 
huffman 
minimize imports

file 
diff 
annotate

Sun, 09 May 2010 14:21:44 0700 
huffman 
remove a couple of redundant lemmas; simplify some proofs

file 
diff 
annotate

Tue, 04 May 2010 13:11:15 0700 
huffman 
merged

file 
diff 
annotate

Tue, 04 May 2010 13:08:56 0700 
huffman 
generalize types of LIMSEQ and LIM; generalize many lemmas

file 
diff 
annotate

Tue, 04 May 2010 10:06:05 0700 
huffman 
make (X > L) an abbreviation for (X > L) sequentially

file 
diff 
annotate

Mon, 03 May 2010 20:42:58 0700 
huffman 
remove unneeded constant Zseq

file 
diff 
annotate

Tue, 04 May 2010 20:26:53 +0200 
wenzelm 
fixed proof (cf. edc381bf7200);

file 
diff 
annotate

Tue, 04 May 2010 17:53:20 +0200 
hoelzl 
Removed unnecessary assumption

file 
diff 
annotate

Fri, 30 Apr 2010 13:31:32 0700 
huffman 
add lemmas about convergent

file 
diff 
annotate

Fri, 12 Mar 2010 15:35:41 +0100 
hoelzl 
Equality of integral and infinite sum.

file 
diff 
annotate

Mon, 22 Feb 2010 20:41:49 +0100 
hoelzl 
Replaced Integration by MultivariateAnalysis/Real_Integration

file 
diff 
annotate

Thu, 18 Feb 2010 14:21:44 0800 
huffman 
get rid of many duplicate simp rule warnings

file 
diff 
annotate

Wed, 28 Oct 2009 11:42:31 +0000 
paulson 
New theory Probability, which contains a development of measure theory

file 
diff 
annotate

Wed, 21 Oct 2009 12:02:56 +0200 
haftmann 
curried union as canonical list operation

file 
diff 
annotate

Sat, 17 Oct 2009 14:43:18 +0200 
wenzelm 
eliminated hard tabulators, guessing at each author's individual tabwidth;

file 
diff 
annotate

Mon, 05 Oct 2009 17:27:46 +0100 
paulson 
New lemmas connected with the reals and infinite series

file 
diff 
annotate

Fri, 25 Sep 2009 13:47:28 +0100 
paulson 
New lemmas involving the real numbers, especially limits and series

file 
diff 
annotate

Fri, 28 Aug 2009 18:52:41 +0200 
nipkow 
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules

file 
diff 
annotate

Tue, 14 Jul 2009 15:54:19 +0200 
haftmann 
refinement of lattice classes

file 
diff 
annotate

Fri, 12 Jun 2009 15:46:21 0700 
huffman 
add lemma tendsto_setsum

file 
diff 
annotate

Sat, 06 Jun 2009 09:11:12 0700 
huffman 
generalize tendsto to class topological_space

file 
diff 
annotate

Fri, 05 Jun 2009 15:59:20 0700 
huffman 
put syntax for tendsto in Limits.thy; rename variables

file 
diff 
annotate

Tue, 02 Jun 2009 23:31:03 0700 
huffman 
generalize type of constant lim

file 
diff 
annotate

Tue, 02 Jun 2009 23:06:05 0700 
huffman 
class complete_space

file 
diff 
annotate

Tue, 02 Jun 2009 17:03:22 0700 
huffman 
replace filters with filter bases

file 
diff 
annotate

Mon, 01 Jun 2009 10:36:42 0700 
huffman 
limits of inverse using filters

file 
diff 
annotate

Mon, 01 Jun 2009 07:57:37 0700 
huffman 
add [code del] declarations

file 
diff 
annotate

Sun, 31 May 2009 21:59:33 0700 
huffman 
new theory of filters and limits; prove LIMSEQ and LIM lemmas using filters

file 
diff 
annotate

Thu, 28 May 2009 22:57:17 0700 
huffman 
generalize constants in SEQ.thy to class metric_space

file 
diff 
annotate

Tue, 28 Apr 2009 15:50:30 +0200 
haftmann 
stripped class recpower further

file 
diff 
annotate

Thu, 26 Mar 2009 14:10:48 +0000 
paulson 
New theorems mostly concerning infinite series.

file 
diff 
annotate

Wed, 04 Mar 2009 17:12:23 0800 
huffman 
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc

file 
diff 
annotate

Wed, 04 Mar 2009 11:05:29 +0100 
blanchet 
Merge.

file 
diff 
annotate

Wed, 04 Mar 2009 10:45:52 +0100 
blanchet 
Merge.

file 
diff 
annotate

Mon, 02 Mar 2009 12:33:12 +0000 
chaieb 
Moved a few theorems about monotonic sequences from Fundamental_Theorem_Algebra to SEQ.thy

file 
diff 
annotate

Tue, 24 Feb 2009 11:12:58 0800 
huffman 
make more proofs work whether or not One_nat_def is a simp rule

file 
diff 
annotate

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

file 
diff 
annotate

Wed, 28 Jan 2009 16:29:16 +0100 
nipkow 
Replaced group_ and ring_simps by algebra_simps;

file 
diff 
annotate

Mon, 29 Dec 2008 14:08:08 +0100 
haftmann 
adapted HOL source structure to distribution layout

file 
diff 
annotate
 base
