src/HOL/Analysis/Bounded_Continuous_Function.thy

     Henstock_Kurzweil_Integration
 begin
 
 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"
   morphisms apply_bcontfun Bcontfun
   by (auto intro: continuous_intros simp: bounded_def bcontfun_def)

 
 (* TODO: Generalize to uniform spaces? *)
 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"
   where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
 

 qed
 
 
 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"
     using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
     unfolding Cauchy_def uniform_limit_sequentially_iff

   then show "convergent f"
     by (intro convergentI)
 qed
 
 
-subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
-
-instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Supremum norm for a normed vector space\<close>
+
+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"
   by (auto simp: bcontfun_def intro!: continuous_intros)
 

 
 lemma bounded_norm_le_SUP_norm:
   "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"
   where "norm_bcontfun f = dist f 0"
 

   assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
   shows "norm f \<le> b"
   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 =
     (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
   by (auto simp: clamp_def)