src/HOL/Analysis/Abstract_Topology_2.thy

     using \<open>T \<subseteq> image f S\<close> \<open>inj f\<close> unfolding inj_on_def subset_eq by auto
   ultimately have "y \<in> interior S" ..
   with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
-subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Equality of continuous functions on closure and related results\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "continuous_on S f \<Longrightarrow> closedin (top_of_set S) {x \<in> S. f x = a}"
   using continuous_closedin_preimage[of S f "{a}"] by (simp add: vimage_def Collect_conj_eq)

   ultimately have "closure S = (closure S \<inter> f -` T)"
     using closure_minimal[of S "(closure S \<inter> f -` T)"] by auto
   then show ?thesis by auto
 qed
 
-subsection%unimportant \<open>A function constant on a set\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>A function constant on a set\<close>
 
 definition constant_on  (infixl "(constant'_on)" 50)
   where "f constant_on A \<equiv> \<exists>y. \<forall>x\<in>A. f x = y"
 
 lemma constant_on_subset: "\<lbrakk>f constant_on A; B \<subseteq> A\<rbrakk> \<Longrightarrow> f constant_on B"

     shows "f constant_on (closure S)"
 using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
 by metis
 
 
-subsection%unimportant \<open>Continuity relative to a union.\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
 
 lemma continuous_on_Un_local:
     "\<lbrakk>closedin (top_of_set (s \<union> t)) s; closedin (top_of_set (s \<union> t)) t;
       continuous_on s f; continuous_on t f\<rbrakk>
      \<Longrightarrow> continuous_on (s \<union> t) f"

     shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms
 by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
 
 
-subsection%unimportant\<open>Inverse function property for open/closed maps\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
   assumes contf: "continuous_on S f"
     and imf: "f ` S = T"
     and injf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"

     by (metis hom homeomorphism_def)
   ultimately show ?thesis
     by (simp add: continuous_on_closed oo)
 qed
 
-subsection%unimportant \<open>Seperability\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Seperability\<close>
 
 lemma subset_second_countable:
   obtains \<B> :: "'a:: second_countable_topology set set"
     where "countable \<B>"
           "{} \<notin> \<B>"

     by (clarsimp simp add: countable_subset_image)
   then show ?thesis ..
 qed
 
 
-subsection%unimportant\<open>Closed Maps\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Closed Maps\<close>
 
 lemma continuous_imp_closed_map:
   fixes f :: "'a::t2_space \<Rightarrow> 'b::t2_space"
   assumes "closedin (top_of_set S) U"
           "continuous_on S f" "f ` S = T" "compact S"

     using cloU by (auto simp: closedin_closed)
   with cc [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
     by (fastforce simp add: closedin_closed)
 qed
 
-subsection%unimportant\<open>Open Maps\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Open Maps\<close>
 
 lemma open_map_restrict:
   assumes opeU: "openin (top_of_set (S \<inter> f -` T')) U"
     and oo: "\<And>U. openin (top_of_set S) U \<Longrightarrow> openin (top_of_set T) (f ` U)"
     and "T' \<subseteq> T"

   with oo [of "S \<inter> V"] \<open>T' \<subseteq> T\<close> show ?thesis
     by (fastforce simp add: openin_open)
 qed
 
 
-subsection%unimportant\<open>Quotient maps\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Quotient maps\<close>
 
 lemma quotient_map_imp_continuous_open:
   assumes T: "f ` S \<subseteq> T"
       and ope: "\<And>U. U \<subseteq> T
               \<Longrightarrow> (openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>

   assumes "continuous_on S f" "f ` S = T" "compact S" "U \<subseteq> T"
     shows "openin (top_of_set S) (S \<inter> f -` U) \<longleftrightarrow>
            openin (top_of_set T) U"
   by (metis (no_types, lifting) assms closed_map_imp_quotient_map continuous_imp_closed_map)
 
-subsection%unimportant\<open>Pasting lemmas for functions, for of casewise definitions\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Pasting lemmas for functions, for of casewise definitions\<close>
 
 subsubsection\<open>on open sets\<close>
 
 lemma pasting_lemma:
   assumes ope: "\<And>i. i \<in> I \<Longrightarrow> openin X (T i)"

     using that continuous_map_frontier_frontier_preimage_subset [OF contp, of U] fg by blast
 qed
 
 subsection \<open>Retractions\<close>
 
-definition%important retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> retraction :: "('a::topological_space) set \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
 where "retraction S T r \<longleftrightarrow>
   T \<subseteq> S \<and> continuous_on S r \<and> r ` S \<subseteq> T \<and> (\<forall>x\<in>T. r x = x)"
 
-definition%important retract_of (infixl "retract'_of" 50) where
+definition\<^marker>\<open>tag important\<close> retract_of (infixl "retract'_of" 50) where
 "T retract_of S  \<longleftrightarrow>  (\<exists>r. retraction S T r)"
 
 lemma retraction_idempotent: "retraction S T r \<Longrightarrow> x \<in> S \<Longrightarrow>  r (r x) = r x"
   unfolding retraction_def by auto