diff -r 1daf07b65385 -r c41954ee87cf src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Tue Jan 01 20:57:54 2019 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Tue Jan 01 21:47:27 2019 +0100
@@ -817,7 +817,7 @@
   then show ?thesis using * by auto
 qed
 
-text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
+text \<open>The next lemma shows that \<open>L\<^sup>1\<close> convergence of a sequence of functions follows from almost
 everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
 just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
 variations) are known as Scheffe lemma.