NEWS
changeset 54787 6d1670095414
parent 54745 46e441e61ff5
child 54850 980817309b78
     1.1 --- a/NEWS	Tue Dec 17 09:52:10 2013 +0100
     1.2 +++ b/NEWS	Tue Dec 17 11:12:10 2013 +0100
     1.3 @@ -110,6 +110,15 @@
     1.4    - Fixed soundness bug whereby mutually recursive datatypes could take
     1.5      infinite values.
     1.6  
     1.7 +* HOL-Multivariate_Analysis:
     1.8 +  - type class ordered_real_vector for ordered vector spaces
     1.9 +  - changed order of ordered_euclidean_space to be compatible with
    1.10 +    pointwise ordering on products. Therefore instance of
    1.11 +    conditionally_complete_lattice and ordered_real_vector.
    1.12 +    INCOMPATIBILITY: use box instead of greaterThanLessThan or
    1.13 +    explicit set-comprehensions with eucl_less for other (half-) open
    1.14 +    intervals.
    1.15 +
    1.16  
    1.17  *** ML ***
    1.18