diff -r c268def0784b -r 264f2b69d09c src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Jun 23 14:43:15 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Mon Jun 26 14:38:19 2023 +0100
@@ -3033,7 +3033,7 @@
 definition homeomorphic_space (infixr "homeomorphic'_space" 50)
   where "X homeomorphic_space Y \<equiv> \<exists>f g. homeomorphic_maps X Y f g"
 
-lemma homeomorphic_space_refl: "X homeomorphic_space X"
+lemma homeomorphic_space_refl [iff]: "X homeomorphic_space X"
   by (meson homeomorphic_maps_id homeomorphic_space_def)
 
 lemma homeomorphic_space_sym: