| Wed, 06 Jun 2007 20:49:04 +0200 |
huffman |
add axclass semiring_char_0 for types where of_nat is injective
|
file |
diff |
annotate
|
| Wed, 30 May 2007 02:41:26 +0200 |
huffman |
simplify names of locale interpretations
|
file |
diff |
annotate
|
| Tue, 29 May 2007 18:19:56 +0200 |
huffman |
interpretation bounded_linear_divide
|
file |
diff |
annotate
|
| Mon, 28 May 2007 04:22:44 +0200 |
huffman |
interpretations additive_scaleR_left, additive_scaleR_right
|
file |
diff |
annotate
|
| Mon, 14 May 2007 20:48:32 +0200 |
huffman |
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
|
file |
diff |
annotate
|
| Mon, 14 May 2007 20:14:31 +0200 |
huffman |
generalized sgn function to work on any real normed vector space
|
file |
diff |
annotate
|
| Sat, 12 May 2007 18:16:30 +0200 |
huffman |
add lemma additive.setsum
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:00:15 +0200 |
huffman |
instance real_algebra_1 < ring_char_0
|
file |
diff |
annotate
|
| Wed, 09 May 2007 22:14:26 +0200 |
huffman |
add lemma norm_diff_ineq; shorten other proofs
|
file |
diff |
annotate
|
| Wed, 09 May 2007 00:27:36 +0200 |
huffman |
add lemmas norm_add_less, norm_mult_less
|
file |
diff |
annotate
|
| Tue, 08 May 2007 18:23:37 +0200 |
huffman |
add lemmas norm_number_of, norm_of_int, norm_of_nat
|
file |
diff |
annotate
|
| Tue, 08 May 2007 04:55:19 +0200 |
huffman |
add lemma abs_norm_cancel
|
file |
diff |
annotate
|
| Mon, 07 May 2007 23:07:04 +0200 |
huffman |
clean up RealVector classes
|
file |
diff |
annotate
|
| Wed, 11 Apr 2007 19:42:43 +0200 |
huffman |
new class syntax for scaleR and norm classes
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 21:51:08 +0200 |
huffman |
interpretation bounded_linear_of_real
|
file |
diff |
annotate
|