src/HOL/Analysis/Abstract_Topology.thy

--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Apr 03 16:38:59 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Apr 04 14:19:33 2019 +0100
@@ -4063,7 +4063,7 @@
   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
 using openin_topology_generated_by_iff by auto
 
-lemma topology_generated_by_topspace:
+lemma topology_generated_by_topspace [simp]:
   "topspace (topology_generated_by S) = (\<Union>S)"
 proof
   {