summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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