News update referring to Analysis
authorpaulson <lp15@cam.ac.uk>
Fri, 14 Jul 2023 14:21:25 +0100
changeset 78333 c515bc9375b9
parent 78332 3b4bbc5b7c46
child 78335 7a6a7f70fadc
News update referring to Analysis
NEWS
--- a/NEWS	Fri Jul 14 09:32:44 2023 +0200
+++ b/NEWS	Fri Jul 14 14:21:25 2023 +0100
@@ -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