# HG changeset patch
# User wenzelm
# Date 1556908519 -7200
# Node ID 8feae28e5c449b43a4c0131d1aca8386b788779b
# Parent  7e9269c188d63edcc429b80d4b72a81decab4a4a# Parent  2ca87b48107777f16e332b35f619b588e3112334
merged

diff -r 2ca87b481077 -r 8feae28e5c44 NEWS
--- a/NEWS	Fri May 03 20:03:45 2019 +0200
+++ b/NEWS	Fri May 03 20:35:19 2019 +0200
@@ -209,7 +209,8 @@
 situations, type conversions are not inserted implicitly any longer
 and need to be given explicitly. Auxiliary abbreviations INFIMUM,
 SUPREMUM, UNION, INTER should now rarely occur in output and are just
-retained as migration auxiliary. INCOMPATIBILITY.
+retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM
+are gone INCOMPATIBILITY.
 
 * The simplifier uses image_cong_simp as a congruence rule. The historic
 and not really well-formed congruence rules INF_cong*, SUP_cong*, are
diff -r 2ca87b481077 -r 8feae28e5c44 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri May 03 20:03:45 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri May 03 20:35:19 2019 +0200
@@ -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