src/HOL/Real/HahnBanach/NormedSpace.thy
 changeset 27612 d3eb431db035 parent 27611 2c01c0bdb385 child 28823 dcbef866c9e2
```     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.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
```