src/HOL/Multivariate_Analysis/Integration.thy

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 03 15:15:00 2012 +0200
@@ -4477,7 +4477,7 @@
 subsection {* Geometric progression *}
 
 text {* FIXME: Should one or more of these theorems be moved to @{file
-"~~/src/HOL/SetInterval.thy"}, alongside @{text geometric_sum}? *}
+"~~/src/HOL/Set_Interval.thy"}, alongside @{text geometric_sum}? *}
 
 lemma sum_gp_basic:
   fixes x :: "'a::ring_1"