src/HOL/Analysis/Connected.thy

 theory Connected
   imports
     Abstract_Topology_2
 begin
 
-subsection%unimportant \<open>Connectedness\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Connectedness\<close>
 
 lemma connected_local:
  "connected S \<longleftrightarrow>
   \<not> (\<exists>e1 e2.
       openin (top_of_set S) e1 \<and>

     by (simp add: th0 th1)
 qed
 
 subsection \<open>Connected components, considered as a connectedness relation or a set\<close>
 
-definition%important "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
+definition\<^marker>\<open>tag important\<close> "connected_component s x y \<equiv> \<exists>t. connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t"
 
 abbreviation "connected_component_set s x \<equiv> Collect (connected_component s x)"
 
 lemma connected_componentI:
   "connected t \<Longrightarrow> t \<subseteq> s \<Longrightarrow> x \<in> t \<Longrightarrow> y \<in> t \<Longrightarrow> connected_component s x y"

   using connected_component_eq_empty by blast
 
 
 subsection \<open>The set of connected components of a set\<close>
 
-definition%important components:: "'a::topological_space set \<Rightarrow> 'a set set"
+definition\<^marker>\<open>tag important\<close> components:: "'a::topological_space set \<Rightarrow> 'a set set"
   where "components s \<equiv> connected_component_set s ` s"
 
 lemma components_iff: "s \<in> components u \<longleftrightarrow> (\<exists>x. x \<in> u \<and> s = connected_component_set u x)"
   by (auto simp: components_def)
 

 lemma closedin_component:
    "C \<in> components s \<Longrightarrow> closedin (top_of_set s) C"
   using closedin_connected_component componentsE by blast
 
 
-subsection%unimportant \<open>Proving a function is constant on a connected set
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Proving a function is constant on a connected set
   by proving that a level set is open\<close>
 
 lemma continuous_levelset_openin_cases:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>

   using continuous_levelset_openin[OF assms(1,2), of a, unfolded openin_open]
   using assms (3,4)
   by fast
 
 
-subsection%unimportant \<open>Preservation of Connectedness\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Preservation of Connectedness\<close>
 
 lemma homeomorphic_connectedness:
   assumes "s homeomorphic t"
   shows "connected s \<longleftrightarrow> connected t"
 using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)

     using * [of "S \<inter> H3" "S \<inter> H4"] \<open>H3 \<inter> H4 = {}\<close> \<open>C \<subseteq> U - S\<close> \<open>H3 \<union> H4 = U - C\<close> \<open>S \<subseteq> U\<close> 
     by auto
 qed
 
 
-subsection%unimportant\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Constancy of a function from a connected set into a finite, disconnected or discrete set\<close>
 
 text\<open>Still missing: versions for a set that is smaller than R, or countable.\<close>
 
 lemma continuous_disconnected_range_constant:
   assumes S: "connected S"