changeset 69617 | 63ee37c519a3 |
parent 69597 | ff784d5a5bfb |
child 69631 | 6c3e6038e74c |
--- a/src/HOL/Analysis/Tagged_Division.thy Mon Jan 07 13:08:50 2019 +0100 +++ b/src/HOL/Analysis/Tagged_Division.thy Mon Jan 07 13:16:33 2019 +0100 @@ -6,7 +6,7 @@ section%important \<open>Tagged divisions used for the Henstock-Kurzweil gauge integration\<close> (*FIXME move together with Henstock_Kurzweil_Integration.thy *) theory Tagged_Division - imports Connected + imports Topology_Euclidean_Space begin term comm_monoid