# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568298759 -3600
# Node ID 8518a750f7bb5b53744518d8932df4dbb40707db
# Parent  67360d50ebb346075044a35f3ed735ee0e86ad5e
importation fix

diff -r 67360d50ebb3 -r 8518a750f7bb src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 12 14:51:50 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 12 15:32:39 2019 +0100
@@ -9,7 +9,7 @@
 theory Elementary_Normed_Spaces
   imports
   "HOL-Library.FuncSet"
-  Elementary_Metric_Spaces
+  Elementary_Metric_Spaces Linear_Algebra
   Connected
 begin