# HG changeset patch
# User paulson
# Date 1556894593 -3600
# Node ID 498ae040d47be111a3301e170438be1dfffdfed6
# Parent  4e08343229819ed3dd9450bd1b1da8e83e6a4ad0# Parent  b0680d8b06082003a12b6a2761c609dc73a5b247
merged

diff -r 4e0834322981 -r 498ae040d47b src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu May 02 22:06:40 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri May 03 15:43:13 2019 +0100
@@ -13,8 +13,7 @@
 subsection \<open>General notion of a topology as a value\<close>
 
 definition\<^marker>\<open>tag important\<close> istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
-"istopology L \<longleftrightarrow>
-  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union>K))"
+  "istopology L \<equiv> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>\<K>. (\<forall>K\<in>\<K>. L K) \<longrightarrow> L (\<Union>\<K>))"
 
 typedef\<^marker>\<open>tag important\<close> 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
@@ -55,7 +54,7 @@
     "openin U {}"
     "\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
     "\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
-  using openin[of U] unfolding istopology_def mem_Collect_eq by fast+
+  using openin[of U] unfolding istopology_def by auto
 
 lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
   unfolding topspace_def by blast