| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 15:46:21 -0700 |
huffman |
add lemma tendsto_setsum
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 11:51:12 -0700 |
huffman |
theorem attribute [tendsto_intros]
|
file |
diff |
annotate
|
| Sun, 07 Jun 2009 17:59:54 -0700 |
huffman |
replace 'topo' with 'open'; add extra type constraint for 'open'
|
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
|
| Thu, 04 Jun 2009 17:24:09 -0700 |
huffman |
generalize type of 'at' to topological_space; generalize some lemmas
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 17:03:22 -0700 |
huffman |
replace filters with filter bases
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 16:27:54 -0700 |
huffman |
declare Bfun_def [code del]
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 10:56:31 -0700 |
huffman |
simp del -> code del
|
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
|