src/HOL/Analysis/Ordered_Euclidean_Space.thy

 lemma in_Basis_prod_iff:
   fixes i::"'a::euclidean_space*'b::euclidean_space"
   shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
   by (cases i) (auto simp: Basis_prod_def)
 
-instantiation%unimportant prod :: (abs, abs) abs
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (abs, abs) abs
 begin
 
 definition "\<bar>x\<bar> = (\<bar>fst x\<bar>, \<bar>snd x\<bar>)"
 
 instance ..

             bounded_subset_cbox_symmetric interval_cbox)
 
 instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
 begin
 
-definition%important "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
-definition%important "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
-definition%important "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
-definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
-definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
+definition\<^marker>\<open>tag important\<close> "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
+definition\<^marker>\<open>tag important\<close> "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
+definition\<^marker>\<open>tag important\<close> "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
+definition\<^marker>\<open>tag important\<close> "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
+definition\<^marker>\<open>tag important\<close> "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
 
 instance
   apply standard
   unfolding euclidean_representation_sum'
   apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis