1.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:50:09 2008 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 19:39:37 2008 +0200
     1.3 @@ -5,7 +5,9 @@
     1.4  
     1.5  header {* Normed vector spaces *}
     1.6  
     1.7 -theory NormedSpace imports  Subspace begin
     1.8 +theory NormedSpace
     1.9 +imports Subspace
    1.10 +begin
    1.11  
    1.12  subsection {* Quasinorms *}
    1.13  
    1.14 @@ -32,7 +34,7 @@
    1.15  proof -
    1.16    interpret vectorspace [V] by fact
    1.17    assume x: "x \<in> V" and y: "y \<in> V"
    1.18 -  hence "x - y = x + - 1 \<cdot> y"
    1.19 +  then have "x - y = x + - 1 \<cdot> y"
    1.20      by (simp add: diff_eq2 negate_eq2a)
    1.21    also from x y have "\<parallel>\<dots>\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>- 1 \<cdot> y\<parallel>"
    1.22      by (simp add: subadditive)
    1.23 @@ -48,7 +50,7 @@
    1.24  proof -
    1.25    interpret vectorspace [V] by fact
    1.26    assume x: "x \<in> V"
    1.27 -  hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    1.28 +  then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    1.29    also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
    1.30      by (rule abs_homogenous)
    1.31    also have "\<dots> = \<parallel>x\<parallel>" by simp
    1.32 @@ -103,7 +105,8 @@
    1.33  proof -
    1.34    interpret subspace [F E] by fact
    1.35    interpret normed_vectorspace [E norm] by fact
    1.36 -  show ?thesis proof
    1.37 +  show ?thesis
    1.38 +  proof
    1.39      show "vectorspace F" by (rule vectorspace) unfold_locales
    1.40    next
    1.41      have "NormedSpace.norm E norm" by unfold_locales