# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1685528911 -3600
# Node ID 8234c42d20e64ee90644b7fec3e795d3611c912f
# Parent  acf27e8352d28f24312cc885dd51dded4e9473dc
NEWS: Announcing the metric space material

diff -r acf27e8352d2 -r 8234c42d20e6 NEWS
--- a/NEWS	Wed May 31 11:05:44 2023 +0100
+++ b/NEWS	Wed May 31 11:28:31 2023 +0100
@@ -301,9 +301,12 @@
 * HOL-Algebra: new theories SimpleGroups (simple groups) 
   and SndIsomorphismGrp (second isomorphism theorem for groups), 
   by Jakob von Raumer
-
-* HOL-Analysis and HOL-Complex_Analysis:  much new material, due to
-   Manuel Eberl and Wenda Li.
+  
+* HOL-Analysis: 
+  - imported the HOL Light abstract metric space library and
+    numerous associated topological developments
+  - new material on infinite sums and integration, due to Manuel Eberl 
+    and Wenda Li.
 
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.