--- 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 =