src/HOL/Real/HahnBanach/Linearform.thy
 changeset 27612 d3eb431db035 parent 27611 2c01c0bdb385 child 29234 60f7fb56f8cd
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:50:09 2008 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 19:39:37 2008 +0200
1.3 @@ -5,7 +5,9 @@
1.4
1.6
1.7 -theory Linearform imports VectorSpace begin
1.8 +theory Linearform
1.9 +imports VectorSpace
1.10 +begin
1.11
1.12  text {*
1.13    A \emph{linear form} is a function on a vector space into the reals
1.14 @@ -25,9 +27,9 @@
1.15  proof -
1.16    interpret vectorspace [V] by fact
1.17    assume x: "x \<in> V"
1.18 -  hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
1.19 -  also from x have "... = (- 1) * (f x)" by (rule mult)
1.20 -  also from x have "... = - (f x)" by simp
1.21 +  then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
1.22 +  also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
1.23 +  also from x have "\<dots> = - (f x)" by simp
1.24    finally show ?thesis .
1.25  qed
1.26
1.27 @@ -37,8 +39,8 @@
1.28  proof -
1.29    interpret vectorspace [V] by fact
1.30    assume x: "x \<in> V" and y: "y \<in> V"
1.31 -  hence "x - y = x + - y" by (rule diff_eq1)
1.32 -  also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
1.33 +  then have "x - y = x + - y" by (rule diff_eq1)
1.34 +  also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
1.35    also have "f (- y) = - f y" using vectorspace V y by (rule neg)
1.36    finally show ?thesis by simp
1.37  qed