1.1 --- a/CONTRIBUTORS	Thu Nov 19 11:51:37 2009 +0100
     1.2 +++ b/CONTRIBUTORS	Thu Nov 19 11:57:30 2009 +0100
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* November 2009: Robert Himmelmann, TUM
     1.8 +  Derivation and Brouwer's fixpoint theorem in Multivariate Analysis
     1.9 +
    1.10  * November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
    1.11    A tabled implementation of the reflexive transitive closure
    1.12  

     2.1 --- a/NEWS	Thu Nov 19 11:51:37 2009 +0100
     2.2 +++ b/NEWS	Thu Nov 19 11:57:30 2009 +0100
     2.3 @@ -96,6 +96,14 @@
     2.4  zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
     2.5  INCOMPATIBILITY.
     2.6  
     2.7 +* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint
     2.8 +theorem.
     2.9 +
    2.10 +* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used
    2.11 +in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the
    2.12 +more usual name.
    2.13 +INCOMPATIBILITY.
    2.14 +
    2.15  * Added theorem List.map_map as [simp]. Removed List.map_compose.
    2.16  INCOMPATIBILITY.
    2.17  

     3.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 19 11:51:37 2009 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 19 11:57:30 2009 +0100
     3.3 @@ -13,8 +13,8 @@
     3.4  (*              (c) Copyright, John Harrison 1998-2008                       *)
     3.5  (* ========================================================================= *)
     3.6  
     3.7 -(* Author:                       John Harrison
     3.8 -   Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
     3.9 +(* Author:                     John Harrison
    3.10 +   Translation from HOL light: Robert Himmelmann, TU Muenchen *)
    3.11  
    3.12  header {* Results connected with topological dimension. *}
    3.13  

     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Nov 19 11:51:37 2009 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Nov 19 11:57:30 2009 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (*  Title:      HOL/Library/Convex_Euclidean_Space.thy
     4.5 -    Author:                       John Harrison
     4.6 -    Translated to from HOL light: Robert Himmelmann, TU Muenchen *)
     4.7 +    Author:                     John Harrison
     4.8 +    Translation from HOL light: Robert Himmelmann, TU Muenchen *)
     4.9  
    4.10  header {* Multivariate calculus in Euclidean space. *}
    4.11