src/HOL/Real/HahnBanach/NormedSpace.thy
changeset 28823 dcbef866c9e2
parent 27612 d3eb431db035
child 29234 60f7fb56f8cd
     1.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4    proof
     1.5      show "vectorspace F" by (rule vectorspace) unfold_locales
     1.6    next
     1.7 -    have "NormedSpace.norm E norm" by unfold_locales
     1.8 +    have "NormedSpace.norm E norm" ..
     1.9      with subset show "NormedSpace.norm F norm"
    1.10        by (simp add: norm_def seminorm_def norm_axioms_def)
    1.11    qed