| changeset 67616 | 1d005f514417 |
| parent 67591 | 6fd9902057f5 |
| child 67702 | 2d9918f5b33c |
--- a/NEWS Thu Feb 15 13:04:36 2018 +0100 +++ b/NEWS Fri Feb 16 10:59:14 2018 +0100 @@ -210,6 +210,9 @@ * Predicate pairwise_coprime abolished, use "pairwise coprime" instead. INCOMPATIBILITY. +* The relator rel_filter on filters has been strengthened to its +canonical categorical definition with better properties. INCOMPATIBILITY. + * HOL-Algebra: renamed (^) to [^] * Session HOL-Analysis: Moebius functions and the Riemann mapping