--- a/src/HOL/Analysis/L2_Norm.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/L2_Norm.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -10,7 +10,7 @@
 
 section \<open>L2 Norm\<close>
 
-definition%important L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
+definition\<^marker>\<open>tag important\<close> L2_set :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> real" where
 "L2_set f A = sqrt (\<Sum>i\<in>A. (f i)\<^sup>2)"
 
 lemma L2_set_cong: