| 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
|
| Wed, 31 Aug 2011 13:51:22 -0700 |
huffman |
remove redundant lemma card_enum
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:42:13 -0700 |
huffman |
arrange everything related to ordered_euclidean_space class together
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:06:50 -0700 |
huffman |
generalize and shorten proof of basis_orthogonal
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 15:35:54 -0700 |
huffman |
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 11:57:42 -0700 |
huffman |
simplify many proofs about subspace and span;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 15:32:40 -0700 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 15:06:13 -0700 |
huffman |
move everything related to 'norm' method into new theory file Norm_Arith.thy
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 12:39:42 -0700 |
huffman |
remove unused lemmas dimensionI, dimension_eq
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 11:56:57 -0700 |
huffman |
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
file |
diff |
annotate
|