# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1651765188 -3600
# Node ID 51e05af57455efb92d706c3ee1e21b7880c48498
# Parent  53a60eae475f720240e12bae9563b1dfa01d5fd1
Added a couple of obvious simprules

diff -r 53a60eae475f -r 51e05af57455 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed May 04 07:20:20 2022 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu May 05 16:39:48 2022 +0100
@@ -19,17 +19,17 @@
   morphisms "openin" "topology"
   unfolding istopology_def by blast
 
-lemma istopology_openin[intro]: "istopology(openin U)"
+lemma istopology_openin[iff]: "istopology(openin U)"
   using openin[of U] by blast
 
-lemma istopology_open: "istopology open"
+lemma istopology_open[iff]: "istopology open"
   by (auto simp: istopology_def)
 
-lemma topology_inverse': "istopology U \<Longrightarrow> openin (topology U) = U"
+lemma topology_inverse' [simp]: "istopology U \<Longrightarrow> openin (topology U) = U"
   using topology_inverse[unfolded mem_Collect_eq] .
 
 lemma topology_inverse_iff: "istopology U \<longleftrightarrow> openin (topology U) = U"
-  using topology_inverse[of U] istopology_openin[of "topology U"] by auto
+  by (metis istopology_openin topology_inverse')
 
 lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
 proof