src/HOL/Analysis/Continuous_Extension.thy

     and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
   using assms by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
 
-corollary%unimportant Tietze_closed_interval:
+corollary\<^marker>\<open>tag unimportant\<close> Tietze_closed_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "cbox a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by auto
 
-corollary%unimportant Tietze_closed_interval_1:
+corollary\<^marker>\<open>tag unimportant\<close> Tietze_closed_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "a \<le> b"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
   apply (rule Dugundji [of "cbox a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
-corollary%unimportant Tietze_open_interval:
+corollary\<^marker>\<open>tag unimportant\<close> Tietze_open_interval:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "box a b \<noteq> {}"
     and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by auto
 
-corollary%unimportant Tietze_open_interval_1:
+corollary\<^marker>\<open>tag unimportant\<close> Tietze_open_interval_1:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> real"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
     and "a < b"
     and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
     "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
   apply (rule Dugundji [of "box a b" U S f])
   using assms by (auto simp: image_subset_iff)
 
-corollary%unimportant Tietze_unbounded:
+corollary\<^marker>\<open>tag unimportant\<close> Tietze_unbounded:
   fixes f :: "'a::{metric_space,second_countable_topology} \<Rightarrow> 'b::real_inner"
   assumes "continuous_on S f"
     and "closedin (top_of_set U) S"
   obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
   apply (rule Dugundji [of UNIV U S f])