# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1689501899 -3600
# Node ID c4cc276821d42e8e431f5ed0ef0779d432122ad4
# Parent  1d71ceb76e061c70a535689204594003ad7a101c
X = trivial_topology rather than topspace X = {}

diff -r 1d71ceb76e06 -r c4cc276821d4 NEWS
--- a/NEWS	Sat Jul 15 23:35:00 2023 +0100
+++ b/NEWS	Sun Jul 16 11:04:59 2023 +0100
@@ -334,6 +334,8 @@
 * 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.
+  - Some results reformulated to use X = trivial_topology rather than
+    topspace X = {}, INCOMPATIBILITY, use null_topspace_iff_trivial 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