1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 08:42:26 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 10 09:23:42 2011 -0700
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Elementary topology in Euclidean space. *}
     1.5  
     1.6  theory Topology_Euclidean_Space
     1.7 -imports SEQ Euclidean_Space "~~/src/HOL/Library/Glbs"
     1.8 +imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs"
     1.9  begin
    1.10  
    1.11  (* to be moved elsewhere *)