--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 17:53:55 2016 +0200
@@ -9152,8 +9152,8 @@
subsection \<open>Geometric progression\<close>
-text \<open>FIXME: Should one or more of these theorems be moved to @{file
-"~~/src/HOL/Set_Interval.thy"}, alongside \<open>geometric_sum\<close>?\<close>
+text \<open>FIXME: Should one or more of these theorems be moved to
+ \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
lemma sum_gp_basic:
fixes x :: "'a::ring_1"