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