# HG changeset patch # User paulson # Date 1689340885 -3600 # Node ID c515bc9375b94f2765053d7fe4c04e11e5c91d85 # Parent 3b4bbc5b7c46a506df21f40414c93da30bcba93f News update referring to Analysis diff -r 3b4bbc5b7c46 -r c515bc9375b9 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 \ A\B rather than f`A \ 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