| Wed, 17 Feb 2010 18:33:45 +0100 |
Added integration to Multivariate-Analysis (upto FTC)
|
file | diff | annotate |
| Tue, 16 Feb 2010 15:16:33 +0100 |
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
|
file | diff | annotate |
| Mon, 08 Feb 2010 14:22:22 +0100 |
dropped accidental duplication of "lin" prefix from cs. 108662d50512
|
file | diff | annotate |
| Fri, 05 Feb 2010 14:33:50 +0100 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| Mon, 25 Jan 2010 16:56:24 +0100 |
Replaced vec1 and dest_vec1 by abbreviation.
|
file | diff | annotate |
| Sun, 10 Jan 2010 18:43:45 +0100 |
Adapted to changes in induct method.
|
file | diff | annotate |
| Thu, 07 Jan 2010 17:41:06 +0100 |
remove overloaded star operator, use specific vector / matrix operators
|
file | diff | annotate |
| Thu, 07 Jan 2010 18:56:39 +0100 |
finite annotation on cartesian product is now implicit.
|
file | diff | annotate |
| Wed, 06 Jan 2010 13:07:30 +0100 |
Made finite cartesian products finite
|
file | diff | annotate |
| Thu, 19 Nov 2009 11:51:37 +0100 |
Renamed vector_less_eq_def to the more usual name vector_le_def.
|
file | diff | annotate |
| Mon, 16 Nov 2009 15:03:23 +0100 |
removed hassize predicate
|
file | diff | annotate |
| Mon, 16 Nov 2009 15:06:34 +0100 |
Added new lemmas to Euclidean Space by Robert Himmelmann
|
file | diff | annotate |
| Tue, 27 Oct 2009 14:46:03 +0000 |
merged
|
file | diff | annotate |
| Fri, 23 Oct 2009 13:23:18 +0200 |
distinguished session for multivariate analysis
|
file | diff | annotate |