diff -r ad6d4a14adb5 -r f03a01a18c6e src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -7,7 +7,7 @@
 
 subsection \<open>Definition\<close>
 
-definition%important "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
+definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
 
 typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
   "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
@@ -41,7 +41,7 @@
 instantiation bcontfun :: (topological_space, metric_space) metric_space
 begin
 
-lift_definition%important dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
+lift_definition\<^marker>\<open>tag important\<close> dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
   is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
 
 definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
@@ -175,8 +175,8 @@
 
 subsection \<open>Complete Space\<close>
 
-instance%important bcontfun :: (metric_space, complete_space) complete_space
-proof%unimportant
+instance\<^marker>\<open>tag important\<close> bcontfun :: (metric_space, complete_space) complete_space
+proof
   fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
   assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
   then obtain g where "uniform_limit UNIV f g sequentially"
@@ -191,9 +191,9 @@
 qed
 
 
-subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Supremum norm for a normed vector space\<close>
 
-instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
+instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_vector
 begin
 
 lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
@@ -247,7 +247,7 @@
   "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
   by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
 
-instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector
+instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_normed_vector
 begin
 
 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
@@ -290,7 +290,7 @@
   using dist_bound[of f 0 b] assms
   by (simp add: dist_norm)
 
-subsection%unimportant \<open>(bounded) continuous extenstion\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>(bounded) continuous extenstion\<close>
 
 lemma integral_clamp:
   "integral {t0::real..clamp t0 t1 x} f =