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