diff -r e393a91f86df -r d26348b667f2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 20 17:58:34 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon May 03 14:35:10 2010 +0200
@@ -6,7 +6,7 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Euclidean_Space Product_Vector Glbs
+imports SEQ Euclidean_Space Glbs
 begin
 
 subsection{* General notion of a topology *}