| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 00:11:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 23:41:21 +0200 |
wenzelm |
tuned proofs;
|
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
|
| Wed, 10 Aug 2011 09:23:42 -0700 |
huffman |
split Linear_Algebra.thy from Euclidean_Space.thy
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 19:33:51 +0200 |
hoelzl |
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:41:04 -0700 |
huffman |
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:05:45 -0700 |
huffman |
move operator norm stuff to new theory file
|
file |
diff |
annotate
|