merged

--- 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

--- 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