author | nipkow |
Mon, 14 Jan 2019 16:47:16 +0100 | |
changeset 69656 | dbffe5f52ec2 |
parent 69655 | 2b56cbb02e8a |
child 69657 | 48bf42e7c73b |
--- a/src/HOL/Analysis/Tagged_Division.thy Mon Jan 14 16:10:56 2019 +0100 +++ b/src/HOL/Analysis/Tagged_Division.thy Mon Jan 14 16:47:16 2019 +0100 @@ -4,7 +4,7 @@ *) section \<open>Tagged Divisions for Henstock-Kurzweil Integration\<close> -(*FIXME move together with Henstock_Kurzweil_Integration.thy *) + theory Tagged_Division imports Topology_Euclidean_Space begin