| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 19:14:23 +0100 |
hoelzl |
moved (b)choice_iff(') to Hilbert_Choice
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Fri, 05 Oct 2012 13:57:48 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 21:24:20 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 23:02:49 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 17:55:56 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 22:45:14 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 08:00:28 -0700 |
huffman |
remove duplicate copy of lemma sqrt_add_le_add_sqrt
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 07:48:59 -0700 |
huffman |
remove redundant lemma real_sum_squared_expand in favor of power2_sum
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 13:57:12 -0700 |
huffman |
remove more duplicate lemmas
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 07:31:33 -0700 |
huffman |
add lemma tendsto_infnorm
|
file |
diff |
annotate
|