--- 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.