| Mon, 02 Oct 2006 18:30:10 +0200 |
huffman |
add lemmas norm_not_less_zero, norm_le_zero_iff
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:47 +0200 |
wenzelm |
tuned definitions/proofs;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 19:04:13 +0200 |
huffman |
rearranged axioms and simp rules for scaleR
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 01:48:30 +0200 |
huffman |
add lemmas about of_real and power
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 00:52:59 +0200 |
huffman |
add lemmas of_int_in_Reals, of_nat_in_Reals
|
file |
diff |
annotate
|
| Sun, 24 Sep 2006 07:14:02 +0200 |
huffman |
real_norm_def [simp]
|
file |
diff |
annotate
|
| Fri, 22 Sep 2006 23:17:39 +0200 |
huffman |
add lemma norm_power
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 06:22:26 +0200 |
huffman |
added classes real_div_algebra and real_field; added lemmas
|
file |
diff |
annotate
|
| Sun, 17 Sep 2006 16:42:38 +0200 |
huffman |
norm_one is now proved from other class axioms
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 19:12:03 +0200 |
huffman |
define new constant of_real for class real_algebra_1;
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 02:35:58 +0200 |
huffman |
add theorem norm_diff_triangle_ineq
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 03:25:17 +0200 |
huffman |
remove conflicting norm syntax
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 06:44:45 +0200 |
huffman |
formalization of vector spaces and algebras over the real numbers
|
file |
diff |
annotate
|