src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 70690 8518a750f7bb
parent 70688 3d894e1cfc75
child 70724 65371451fde8
--- 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