| 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 |
| Mon, 26 Apr 2010 15:22:03 -0700 | huffman | move proof of Fashoda meet theorem into separate file | file | diff | annotate |
| Mon, 22 Feb 2010 20:41:49 +0100 | hoelzl | Replaced Integration by Multivariate-Analysis/Real_Integration | file | diff | annotate |
| Wed, 17 Feb 2010 18:56:34 +0100 | hoelzl | Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration. | file | diff | annotate |
| Wed, 17 Feb 2010 18:33:45 +0100 | himmelma | Added integration to Multivariate-Analysis (upto FTC) | file | diff | annotate |
| Tue, 17 Nov 2009 18:52:30 +0100 | hoelzl | Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light) | file | diff | annotate |