--- a/CONTRIBUTORS Thu Nov 19 11:51:37 2009 +0100
+++ b/CONTRIBUTORS Thu Nov 19 11:57:30 2009 +0100
@@ -7,6 +7,9 @@
Contributions to this Isabelle version
--------------------------------------
+* November 2009: Robert Himmelmann, TUM
+ Derivation and Brouwer's fixpoint theorem in Multivariate Analysis
+
* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
A tabled implementation of the reflexive transitive closure
--- a/NEWS Thu Nov 19 11:51:37 2009 +0100
+++ b/NEWS Thu Nov 19 11:57:30 2009 +0100
@@ -96,6 +96,14 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
+* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint
+theorem.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used
+in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the
+more usual name.
+INCOMPATIBILITY.
+
* Added theorem List.map_map as [simp]. Removed List.map_compose.
INCOMPATIBILITY.
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Nov 19 11:51:37 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Nov 19 11:57:30 2009 +0100
@@ -13,8 +13,8 @@
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
-(* Author: John Harrison
- Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
+(* Author: John Harrison
+ Translation from HOL light: Robert Himmelmann, TU Muenchen *)
header {* Results connected with topological dimension. *}
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Nov 19 11:51:37 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Nov 19 11:57:30 2009 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Library/Convex_Euclidean_Space.thy
- Author: John Harrison
- Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
+ Author: John Harrison
+ Translation from HOL light: Robert Himmelmann, TU Muenchen *)
header {* Multivariate calculus in Euclidean space. *}