| 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 |
locale-ize 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 Multivariate-Analysis/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 tab-width;
|
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 type-specific 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
|