| Wed, 17 Feb 2010 18:33:45 +0100 |
Added integration to Multivariate-Analysis (upto FTC)
|
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, 01 Feb 2010 14:12:12 +0100 |
Removed explicit type annotations
|
file | diff | annotate |
| Mon, 25 Jan 2010 16:56:24 +0100 |
Replaced vec1 and dest_vec1 by abbreviation.
|
file | diff | annotate |
| Fri, 15 Jan 2010 08:27:21 +0100 |
spurious proof failure
|
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 |
| Sun, 29 Nov 2009 22:27:47 -0800 |
make proof use only abstract properties of eventually
|
file | diff | annotate |
| Thu, 19 Nov 2009 11:57:30 +0100 |
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS
|
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 |
| Tue, 17 Nov 2009 18:52:30 +0100 |
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
|
file | diff | annotate |