diff -r ad6d4a14adb5 -r f03a01a18c6e src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -9,7 +9,7 @@
 text\<open>The definition here only really makes sense for an elementary set. 
      We just use compact intervals in applications below.\<close>
 
-definition%important equiintegrable_on (infixr "equiintegrable'_on" 46)
+definition\<^marker>\<open>tag important\<close> equiintegrable_on (infixr "equiintegrable'_on" 46)
   where "F equiintegrable_on I \<equiv>
          (\<forall>f \<in> F. f integrable_on I) \<and>
          (\<forall>e > 0. \<exists>\<gamma>. gauge \<gamma> \<and>