author | paulson <lp15@cam.ac.uk> |
Fri, 14 Jul 2023 14:21:25 +0100 | |
changeset 78333 | c515bc9375b9 |
parent 78332 | 3b4bbc5b7c46 |
child 78335 | 7a6a7f70fadc |
--- 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