src/HOL/Analysis/Elementary_Normed_Spaces.thy
changeset 70690 8518a750f7bb
parent 70688 3d894e1cfc75
child 70724 65371451fde8
equal deleted inserted replaced
70689:67360d50ebb3 70690:8518a750f7bb
     7 section \<open>Elementary Normed Vector Spaces\<close>
     7 section \<open>Elementary Normed Vector Spaces\<close>
     8 
     8 
     9 theory Elementary_Normed_Spaces
     9 theory Elementary_Normed_Spaces
    10   imports
    10   imports
    11   "HOL-Library.FuncSet"
    11   "HOL-Library.FuncSet"
    12   Elementary_Metric_Spaces
    12   Elementary_Metric_Spaces Linear_Algebra
    13   Connected
    13   Connected
    14 begin
    14 begin
    15 
    15 
    16 subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
    16 subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
    17 
    17