# HG changeset patch
# User hoelzl
# Date 1258628250 -3600
# Node ID b369324fc244c6a6ef3ce950be48ef3889138eb4
# Parent  53078b0d21f5ae61c61bb39e9f20894786e4a35a
Added the contributions of Robert Himmelmann to CONTRIBUTIONS and NEWS

diff -r 53078b0d21f5 -r b369324fc244 CONTRIBUTORS
--- 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
 
diff -r 53078b0d21f5 -r b369324fc244 NEWS
--- 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.
 
diff -r 53078b0d21f5 -r b369324fc244 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- 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. *}
 
diff -r 53078b0d21f5 -r b369324fc244 src/HOL/Multivariate_Analysis/Derivative.thy
--- 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. *}