NEWS
changeset 68072 493b818e8e10
parent 67999 1b05f74f2e5f
child 68073 fad29d2a17a5
     1.1 --- a/NEWS	Wed Apr 18 21:12:50 2018 +0100
     1.2 +++ b/NEWS	Wed May 02 13:49:38 2018 +0200
     1.3 @@ -257,6 +257,15 @@
     1.4  * The relator rel_filter on filters has been strengthened to its 
     1.5  canonical categorical definition with better properties. INCOMPATIBILITY.
     1.6  
     1.7 +* Generalized linear algebra involving linear, span, dependent, dim
     1.8 +from type class real_vector to locales module and vector_space.
     1.9 +Renamed:
    1.10 +  - span_inc ~> span_superset
    1.11 +  - span_superset ~> span_base
    1.12 +  - span_eq ~> span_eq_iff
    1.13 +INCOMPATIBILITY.
    1.14 +
    1.15 +
    1.16  * HOL-Algebra: renamed (^) to [^]
    1.17  
    1.18  * Session HOL-Analysis: Moebius functions, the Riemann mapping