| 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
|
| Wed, 14 Mar 2007 21:40:28 +0100 |
huffman |
move bounded (bi)linear operator locales from Lim.thy to RealVector.thy
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 00:02:53 +0100 |
huffman |
remove uses of scaleR infix syntax; add lemma Reals_number_of
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| 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
|