--- a/NEWS Tue Dec 17 09:52:10 2013 +0100
+++ b/NEWS Tue Dec 17 11:12:10 2013 +0100
@@ -110,6 +110,15 @@
- Fixed soundness bug whereby mutually recursive datatypes could take
infinite values.
+* HOL-Multivariate_Analysis:
+ - type class ordered_real_vector for ordered vector spaces
+ - changed order of ordered_euclidean_space to be compatible with
+ pointwise ordering on products. Therefore instance of
+ conditionally_complete_lattice and ordered_real_vector.
+ INCOMPATIBILITY: use box instead of greaterThanLessThan or
+ explicit set-comprehensions with eucl_less for other (half-) open
+ intervals.
+
*** ML ***