Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
importation fix
authorpaulson <lp15@cam.ac.uk>
Thu, 12 Sep 2019 15:32:39 +0100
changeset 70690 8518a750f7bb
parent 70689 67360d50ebb3
child 70691 7e93a10b21f0
importation fix
src/HOL/Analysis/Elementary_Normed_Spaces.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle