src/HOL/Analysis/Abstract_Topology.thy

--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -12,11 +12,11 @@
 
 subsection \<open>General notion of a topology as a value\<close>
 
-definition%important istopology :: "('a set \<Rightarrow> bool) \<Rightarrow> bool" where
+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))"
 
-typedef%important 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef\<^marker>\<open>tag important\<close> 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
   unfolding istopology_def by blast
 
@@ -116,7 +116,7 @@
 
 subsubsection \<open>Closed sets\<close>
 
-definition%important closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> closedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
 "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
 
 lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
@@ -240,7 +240,7 @@
 
 subsection \<open>Subspace topology\<close>
 
-definition%important subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
+definition\<^marker>\<open>tag important\<close> subtopology :: "'a topology \<Rightarrow> 'a set \<Rightarrow> 'a topology" where
 "subtopology U V = topology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
 
 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
@@ -415,7 +415,7 @@
 
 subsection \<open>The canonical topology from the underlying type class\<close>
 
-abbreviation%important euclidean :: "'a::topological_space topology"
+abbreviation\<^marker>\<open>tag important\<close> euclidean :: "'a::topological_space topology"
   where "euclidean \<equiv> topology open"
 
 abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
@@ -1416,7 +1416,7 @@
   by (simp add: Sup_le_iff closure_of_minimal)
 
 
-subsection%important \<open>Continuous maps\<close>
+subsection\<^marker>\<open>tag important\<close> \<open>Continuous maps\<close>
 
 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
 of type classes, as defined below.\<close>
@@ -1728,7 +1728,7 @@
 declare continuous_map_id_subt [unfolded id_def, simp]
 
 
-lemma%important continuous_map_alt:
+lemma\<^marker>\<open>tag important\<close> continuous_map_alt:
    "continuous_map T1 T2 f 
     = ((\<forall>U. openin T2 U \<longrightarrow> openin T1 (f -` U \<inter> topspace T1)) \<and> f ` topspace T1 \<subseteq> topspace T2)"
   by (auto simp: continuous_map_def vimage_def image_def Collect_conj_eq inf_commute)
@@ -3793,7 +3793,7 @@
   shows "continuous_map euclidean (top_of_set S) f"
   by (simp add: cont continuous_map_into_subtopology eq image_subset_iff_subset_vimage)
 
-subsection%unimportant \<open>Half-global and completely global cases\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen:
   assumes "continuous_on S f"  "open T"
@@ -4027,7 +4027,7 @@
   using assms by (simp add: Lim_transform_within_openin continuous_within)
 
 
-subsection%important \<open>The topology generated by some (open) subsets\<close>
+subsection\<^marker>\<open>tag important\<close> \<open>The topology generated by some (open) subsets\<close>
 
 text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
 as it follows from \<open>UN\<close> taking for \<open>K\<close> the empty set. However, it is convenient to have,
@@ -4057,7 +4057,7 @@
 using assms(3) apply (induct rule: generate_topology_on.induct)
 using assms(1) assms(2) unfolding istopology_def by auto
 
-abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+abbreviation\<^marker>\<open>tag unimportant\<close> topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
   where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
 
 lemma openin_topology_generated_by_iff:
@@ -4254,7 +4254,7 @@
   using assms continuous_on_generated_topo_iff by blast
 
 
-subsection%important \<open>Pullback topology\<close>
+subsection\<^marker>\<open>tag important\<close> \<open>Pullback topology\<close>
 
 text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
 a special case of this notion, pulling back by the identity. We introduce the general notion as
@@ -4264,7 +4264,7 @@
 text \<open>\<open>pullback_topology A f T\<close> is the pullback of the topology \<open>T\<close> by the map \<open>f\<close> on
 the set \<open>A\<close>.\<close>
 
-definition%important pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
+definition\<^marker>\<open>tag important\<close> pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
   where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-`U \<inter> A)"
 
 lemma istopology_pullback_topology: