author | paulson <lp15@cam.ac.uk> |
Thu, 12 Sep 2019 15:32:39 +0100 | |
changeset 70690 | 8518a750f7bb |
parent 70689 | 67360d50ebb3 |
child 70691 | 7e93a10b21f0 |
--- 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