| Tue, 04 May 2010 10:42:47 -0700 |
huffman |
make (f -- a --> x) an abbreviation for (f ---> x) (at a)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 10:06:05 -0700 |
huffman |
make (X ----> L) an abbreviation for (X ---> L) sequentially
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 09:37:24 -0700 |
huffman |
convert proofs to Isar-style
|
file |
diff |
annotate
|
| Sun, 29 Nov 2009 11:31:39 -0800 |
huffman |
add lemmas open_image_fst, open_image_snd
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 16:23:07 -0700 |
huffman |
declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 12:00:30 -0700 |
huffman |
remove simp add: norm_scaleR
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 16:26:06 -0700 |
huffman |
add lemmas about closed sets
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 11:51:12 -0700 |
huffman |
theorem attribute [tendsto_intros]
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 09:03:24 -0700 |
huffman |
cleaned up some proofs
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 08:26:08 -0700 |
huffman |
new lemmas
|
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
|
| Sun, 07 Jun 2009 15:18:52 -0700 |
huffman |
generalize tendsto lemmas for products
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 09:58:11 -0700 |
huffman |
replace class open with class topo
|
file |
diff |
annotate
|
| Wed, 03 Jun 2009 08:43:29 -0700 |
huffman |
instance * :: topological_space
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 23:35:52 -0700 |
huffman |
instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 16:59:56 -0700 |
huffman |
limits of Pair using filters
|
file |
diff |
annotate
|
| Fri, 29 May 2009 09:58:14 -0700 |
huffman |
instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
|
file |
diff |
annotate
|
| Thu, 28 May 2009 17:09:51 -0700 |
huffman |
define dist for products
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 08:02:11 -0800 |
huffman |
add theory of products as real vector spaces to Library
|
file |
diff |
annotate
|