| Mon, 03 Dec 2012 18:19:12 +0100 |
hoelzl |
use filterlim in Lim and SEQ; tuned proofs
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 10:52:08 -0700 |
huffman |
add lemmas within_empty and tendsto_bot;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 20:56:49 -0700 |
huffman |
move class perfect_space into RealVector.thy;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2011 16:28:07 -0700 |
huffman |
generalize LIM_zero lemmas to arbitrary filters
|
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, 26 Aug 2011 08:12:38 -0700 |
huffman |
add lemma sequentially_imp_eventually_within;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 15:54:43 -0700 |
huffman |
Lim.thy: legacy theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 14:46:45 -0700 |
huffman |
delete unused lemmas about limits
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 11:49:53 -0700 |
huffman |
add lemma isCont_tendsto_compose
|
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
|
| Wed, 17 Aug 2011 13:10:11 -0700 |
huffman |
Lim.thy: generalize and simplify proofs of LIM/LIMSEQ theorems
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 11:39:09 -0700 |
huffman |
add lemma tendsto_compose_eventually; use it to shorten some proofs
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 11:06:39 -0700 |
huffman |
add lemma metric_tendsto_imp_tendsto
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 09:31:23 -0700 |
huffman |
add simp rules for isCont
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 16:48:05 -0700 |
huffman |
add lemma tendsto_compose
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 16:18:13 -0700 |
huffman |
remove extraneous subsection heading
|
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
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 04 May 2010 15:44:42 -0700 |
huffman |
generalize more lemmas about limits
|
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:42:47 -0700 |
huffman |
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 13:17:17 +0200 |
hoelzl |
correct variable order in approximate-method
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 15:36:55 +0200 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
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
|
| 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 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
|