src/HOL/ex/Gauge_Integration.thy

--- a/src/HOL/ex/Gauge_Integration.thy	Fri Aug 05 18:34:57 2016 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy	Mon Aug 08 14:13:14 2016 +0200
@@ -1,7 +1,8 @@
 (*  Author:     Jacques D. Fleuriot, University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
 
-    Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
+    Replaced by ~~/src/HOL/Analysis/Henstock_Kurzweil_Integration and
+    Bochner_Integration.
 *)
 
 section\<open>Theory of Integration on real intervals\<close>