# HG changeset patch
# User wenzelm
# Date 1709666434 -3600
# Node ID b053bd598887b1a9206c31aa0a542cac01536a5b
# Parent  58911207815086ecf0f81919c055b9250a0591e7
avoid suspicious Unicode;

diff -r 589112078150 -r b053bd598887 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Tue Mar 05 20:13:20 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Tue Mar 05 20:20:34 2024 +0100
@@ -1746,7 +1746,7 @@
 
 text \<open>We aim to lift results from the real case to arbitrary Banach spaces. 
       Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}. 
-      The theorem allows us to make statements about a function’s value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
+      The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
 
 text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof. 
       While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.