src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63680 6e1e8b5abbfa
parent 63659 abe0c3872d8a
child 63721 492bb53c3420
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -9152,8 +9152,8 @@
     1.4  
     1.5  subsection \<open>Geometric progression\<close>
     1.6  
     1.7 -text \<open>FIXME: Should one or more of these theorems be moved to @{file
     1.8 -"~~/src/HOL/Set_Interval.thy"}, alongside \<open>geometric_sum\<close>?\<close>
     1.9 +text \<open>FIXME: Should one or more of these theorems be moved to
    1.10 +  \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
    1.11  
    1.12  lemma sum_gp_basic:
    1.13    fixes x :: "'a::ring_1"