# HG changeset patch
# User Lukas Stevens <mail@lukas-stevens.de>
# Date 1689342865 -7200
# Node ID 7a6a7f70fadc2829f98dbd3648d4d234c633ed75
# Parent  530f8dc04d8318931f5b9dd13ce7c6d837b1f305# Parent  c515bc9375b94f2765053d7fe4c04e11e5c91d85
merged;

diff -r 530f8dc04d83 -r 7a6a7f70fadc NEWS
--- a/NEWS	Fri Jul 14 15:45:50 2023 +0200
+++ b/NEWS	Fri Jul 14 15:54:25 2023 +0200
@@ -332,6 +332,8 @@
 by Jakob von Raumer.
 
 * Session "HOL-Analysis":
+  - Some results reformulated to use f \<in> A\<rightarrow>B rather than f`A \<subseteq> B,
+    INCOMPATIBILITY, use image_subset_iff_funcset to fix.
   - Imported the HOL Light abstract metric space library and numerous
     results in abstract topology (1200+ lemmas).
   - New material on infinite sums and integration, due to Manuel Eberl