NEWS
changeset 33759 b369324fc244
parent 33673 881a13cbff2e
child 33818 aa00c583f594
--- 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.