src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy

     (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
       in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
       inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
       eucl_le[where 'a='b] abs_prod_def abs_inner)
 
-text\<open>Instantiation for intervals on @{text ordered_euclidean_space}\<close>
+text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
 
 lemma
   fixes a :: "'a::ordered_euclidean_space"
   shows cbox_interval: "cbox a b = {a..b}"
     and interval_cbox: "{a..b} = cbox a b"